Effective Cartier divisors as closed subschemes

An effective Cartier divisor on a scheme is a closed subscheme whose ideal is locally generated by a nonzerodivisor. We express this using Scheme.IdealSheafData, which already constructs the closed subscheme I.subscheme and its closed immersion I.subschemeι. No integrality or reducedness assumption is imposed on the ambient scheme.

Scheme.IdealSheafData.IsEffectiveCartier uses ordinary ideals of sections on affine opens. The equivalent isEffectiveCartier_iff_exists_comap formulation describes the actual restriction of the ideal sheaf to each affine open. It transports local equations under flat pullback and identifies the resulting closed subscheme with the fibre product through Mathlib's Scheme.IdealSheafData.comapIso. By isEffectiveCartier_iff_exists_isOpenImmersion, the local equations may also be given on affine schemes openly immersed in X, such as the charts Spec (A ⊗[R] B) of a fibre product.

Restriction between affine opens is flat, so a nonzerodivisor on an affine open U remains a nonzerodivisor on every open subset of U, affine or not (IsAffineOpen.isSMulRegular_map). In particular, local equations can be shrunk into any neighbourhood (IsEffectiveCartier.exists_eq_span_singleton_le).

The empty closed subscheme is an effective Cartier divisor, with equation 1. Equations need not generate proper ideals; a zero equation is permitted only on the empty scheme.

References

• Stacks Project, Divisors, Effective Cartier divisors, Tag 01WQ.
• Mathlib's Scheme.IdealSheafData.subscheme and Scheme.IdealSheafData.comapIso supply the closed subscheme and its base change.

theorem AlgebraicGeometry.IsAffineOpen.isSMulRegular_map {X : Scheme} {U V : X.Opens} (hU : IsAffineOpen U) (hVU : V ≤ U) {a : ↑(X.presheaf.obj (Opposite.op U))} (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op U))) a) : IsSMulRegular (↑(X.presheaf.obj (Opposite.op V))) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE hVU).op)) a)

A nonzerodivisor on an affine open U restricts to a nonzerodivisor on every open subset V ⊆ U, affine or not.

def AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier {X : Scheme} (I : X.IdealSheafData) : Prop

An ideal sheaf defines an effective Cartier divisor if near every point its ideal on an affine open is generated by an element whose multiplication map is injective.

Equations

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_iff {X : Scheme} (I : X.IdealSheafData) : I.IsEffectiveCartier ↔ ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (a : ↑(X.presheaf.obj (Opposite.op ↑U))), IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) a ∧ I.ideal U = Ideal.span {a}

The affine local equations characterizing an effective Cartier divisor.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.exists_eq_span_singleton_le {X : Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) (W : X.Opens) {x : ↥X} (hx : x ∈ W) : ∃ (U : ↑X.affineOpens), ↑U ≤ W ∧ x ∈ ↑U ∧ ∃ (a : ↑(X.presheaf.obj (Opposite.op ↑U))), IsSMulRegular (↑(X.presheaf.obj (Opposite.op ↑U))) a ∧ I.ideal U = Ideal.span {a}

A nonzerodivisor equation can be chosen inside any prescribed open neighbourhood.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_top (X : Scheme) : ⊤.IsEffectiveCartier

The empty closed subscheme is an effective Cartier divisor on every scheme.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_ofIdealTop_span_singleton {X : Scheme} [IsAffine X] (a : ↑(X.presheaf.obj (Opposite.op ⊤))) (ha : IsSMulRegular (↑(X.presheaf.obj (Opposite.op ⊤))) a) : (ofIdealTop (Ideal.span {a})).IsEffectiveCartier

On an affine scheme, a global nonzerodivisor cuts out an effective Cartier divisor. The equation may be a unit, in which case the closed subscheme is empty.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_iff_exists_comap {X : Scheme} (I : X.IdealSheafData) : I.IsEffectiveCartier ↔ ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (a : ↑((↑↑U).presheaf.obj (Opposite.op ⊤))), IsSMulRegular (↑((↑↑U).presheaf.obj (Opposite.op ⊤))) a ∧ I.comap (↑U).ι = ofIdealTop (Ideal.span {a})

Effective Cartier equations can equivalently be given on the affine open subschemes themselves, with exact equality of their restricted ideal sheaves.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_iff_exists_isOpenImmersion {X : Scheme} (I : X.IdealSheafData) : I.IsEffectiveCartier ↔ ∀ (x : ↥X), ∃ (Y : Scheme) (_ : IsAffine Y) (φ : Y ⟶ X) (_ : IsOpenImmersion φ), x ∈ Set.range ⇑φ ∧ ∃ (a : ↑(Y.presheaf.obj (Opposite.op ⊤))), IsSMulRegular (↑(Y.presheaf.obj (Opposite.op ⊤))) a ∧ I.comap φ = ofIdealTop (Ideal.span {a})

Effective Cartier equations can equivalently be given on any affine schemes openly immersed in X, not only on the affine open subschemes of X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.comap {X Y : Scheme} {I : Y.IdealSheafData} (hI : I.IsEffectiveCartier) (f : X ⟶ Y) [Flat f] : (I.comap f).IsEffectiveCartier

Pullback along a flat morphism preserves effective Cartier divisors on arbitrary schemes. The pulled-back ideal defines the usual fibre-product closed subscheme.