Effectivity under the Weil–Cartier correspondence

On a Noetherian integral scheme of dimension at most one, regular in codimension one, the Cartier divisor associated with a Weil divisor is effective exactly when the Weil divisor has nonnegative coefficients. The comparison uses the common sheaf of rational sections: effectivity says that the constant rational section 1 belongs to 𝒪_X(D).

The result identifies the effective submonoids of Weil and Cartier divisors. It allows effective divisors used in linear systems and Abel maps to be viewed as effective Cartier divisors.

The comparison uses Scheme.CartierDivisor.isEffective_iff_one_mem_sections and Scheme.CartierDivisor.sections_eq_toWeilDivisor; the effective monoid equivalence is the restriction of SchemeWeilDivisor.equivCartierDivisor.

References

• R. Hartshorne, Algebraic Geometry, II.6.11.
• The Stacks Project, Divisors, Tag 0BE9.

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.isEffective_iff_toWeilDivisor {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : CartierDivisor X) : D.IsEffective ↔ WeilDivisor.IsEffective D.toWeilDivisor

On a Noetherian integral scheme of dimension at most one, regular in codimension one, a Cartier divisor is effective if and only if every coefficient of its associated Weil divisor is nonnegative.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isEffective_equivCartierDivisor_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : SchemeWeilDivisor X) : ((equivCartierDivisor hX) D).IsEffective ↔ WeilDivisor.IsEffective D

The Weil–Cartier equivalence preserves effectivity.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.effectiveEquivCartierDivisor {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) : ↥(WeilDivisor.effectiveSubmonoid (CodimensionOnePoint X)) ≃+ ↥(Scheme.CartierDivisor.effectiveSubmonoid X)

The Weil–Cartier equivalence restricts to an additive equivalence of effective divisors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.effectiveEquivCartierDivisor_apply {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : ↥(WeilDivisor.effectiveSubmonoid (CodimensionOnePoint X))) : ↑((effectiveEquivCartierDivisor hX) D) = (equivCartierDivisor hX) ↑D

On underlying divisors, the effective equivalence is the Weil–Cartier equivalence.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.effectiveEquivCartierDivisor_symm_apply {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [∀ (x : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑x)] (hX : ∀ (x : ↥X), Order.coheight x ≤ 1) (D : ↥(Scheme.CartierDivisor.effectiveSubmonoid X)) : ↑((effectiveEquivCartierDivisor hX).symm D) = (↑D).toWeilDivisor

On underlying divisors, the inverse effective equivalence takes the associated Weil divisor.