Effective Cartier divisors on integral schemes

A Cartier divisor is effective when its local equations are regular at every point. On an integral scheme, a nonzero local equation is automatically a nonzerodivisor. This absolute divisor construction supports the divisor and line-bundle dictionary and, later, relative effective Cartier divisors in families of curves.

Effectivity can be checked using one local equation at each point. Equivalently, the constant section 1 of the rational-function sheaf belongs to 𝒪_X(D) globally. For a principal Cartier divisor, effectivity says that its defining rational function is a global regular function. The zero divisor is effective, and sums of effective divisors are effective.

The local-equation definition follows the Stacks Project, Divisors, Tag 01WQ. The sheaf criterion uses the construction of 𝒪_X(D) in CartierDivisor/Sheaf.

def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.IsEffective {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) : Prop

A Cartier divisor is effective if each of its local equations is regular at the point where it is an equation. Since X is integral, these nonzero equations are nonzerodivisors.

Equations

• D.IsEffective = ∀ (x : ↥X) (f : (↑X.functionField)ˣ), D.IsLocalEquationAt x f → ↑f ∈ (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField).range

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_iff_exists {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D : CartierDivisor X} : D.IsEffective ↔ ∀ (x : ↥X), ∃ (f : (↑X.functionField)ˣ), D.IsLocalEquationAt x f ∧ ↑f ∈ (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField).range

To check effectivity, it suffices to find one regular local equation at every point.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_zero {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : IsEffective 0

The zero Cartier divisor is effective.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.IsEffective.add {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D E : CartierDivisor X} (hD : D.IsEffective) (hE : E.IsEffective) : (D + E).IsEffective

The sum of two effective Cartier divisors is effective.

def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.effectiveSubmonoid (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] : AddSubmonoid (CartierDivisor X)

Effective Cartier divisors form an additive submonoid.

Equations

• TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.effectiveSubmonoid X = { carrier := {D : TauCeti.AlgebraicGeometry.Scheme.CartierDivisor X | D.IsEffective}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.mem_effectiveSubmonoid {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) : D ∈ effectiveSubmonoid X ↔ D.IsEffective

Membership in the effective Cartier divisor submonoid is effectivity.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_iff_one_mem_sections {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D : CartierDivisor X} : D.IsEffective ↔ (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (toRationalFunctions X) ⊤)) 1 ∈ D.sections ⊤

Effectivity can be tested by the single global section 1 of 𝒪_X.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_iff_toRationalFunctions_mem_sections {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D : CartierDivisor X} : D.IsEffective ↔ ∀ (U : X.Opens) (s : ↑(X.presheaf.obj (Opposite.op U))), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (toRationalFunctions X) U)) s ∈ D.sections U

A Cartier divisor is effective exactly when the regular functions are sections of 𝒪_X(D) under the canonical inclusion into rational functions.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.unitToSheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) (hD : D.IsEffective) : SheafOfModules.unit X.ringCatSheaf ⟶ D.sheaf

An effective Cartier divisor has the canonical inclusion 𝒪_X ⟶ 𝒪_X(D). Its composite with 𝒪_X(D) ⟶ 𝒦_X is the usual inclusion of regular functions into rational functions.

Equations

• D.unitToSheaf hD = D.sheafLift (TauCeti.AlgebraicGeometry.Scheme.toRationalFunctions X) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.unitToSheaf_ι {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) (hD : D.IsEffective) : CategoryTheory.CategoryStruct.comp (D.unitToSheaf hD) D.sheafι = toRationalFunctions X

The inclusion 𝒪_X ⟶ 𝒪_X(D) of an effective Cartier divisor agrees with the usual inclusion after embedding both sheaves in rational functions.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.unitToSheaf_ι_assoc {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) (hD : D.IsEffective) {Z : SheafOfModules X.ringCatSheaf} (h : rationalFunctions X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (D.unitToSheaf hD) D.sheafι) h = CategoryTheory.CategoryStruct.comp (toRationalFunctions X) h

The inclusion 𝒪_X ⟶ 𝒪_X(D) of an effective Cartier divisor agrees with the usual inclusion after embedding both sheaves in rational functions.

instance TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.instMonoSheafOfModulesOpensCarrierCarrierCommRingCatRingCatSheafUnitToSheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) (hD : D.IsEffective) : CategoryTheory.Mono (D.unitToSheaf hD)

The canonical map from regular functions to the sheaf of an effective Cartier divisor is a monomorphism.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_iff_exists_unitToSheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] {D : CartierDivisor X} : D.IsEffective ↔ ∃ (φ : SheafOfModules.unit X.ringCatSheaf ⟶ D.sheaf), CategoryTheory.CategoryStruct.comp φ D.sheafι = toRationalFunctions X

Effectivity is equivalent to the existence of a map 𝒪_X ⟶ 𝒪_X(D) whose composite with the inclusion into rational functions is the usual inclusion of regular functions.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.eq_unitToSheaf {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (D : CartierDivisor X) (hD : D.IsEffective) (φ : SheafOfModules.unit X.ringCatSheaf ⟶ D.sheaf) (hφ : CategoryTheory.CategoryStruct.comp φ D.sheafι = toRationalFunctions X) : φ = D.unitToSheaf hD

The map from regular functions to 𝒪_X(D) is determined by its composite with the inclusion into rational functions.

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_principalCartierDivisor_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (f : (↑X.functionField)ˣ) : (principalCartierDivisor X f).IsEffective ↔ ∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a = ↑f

A principal Cartier divisor is effective exactly when its rational equation is regular on the whole scheme.