Relative effective Cartier divisors

An effective Cartier divisor on X relative to S is an effective Cartier divisor whose closed subscheme is flat over S. This file shows that relative effective Cartier divisors are stable under arbitrary base change T ⟶ S, with no flatness assumption on T ⟶ S or on X over S, so pullback along any T ⟶ S carries relative effective Cartier divisors on X over S to relative effective Cartier divisors on X ×_S T over T. The base change may be taken along any pullback square, which is what makes T ↦ {relative effective Cartier divisors on X ×_S T} functorial in T.

Over affine opens W ⊆ S and U ⊆ X lying over it, a local equation a of the divisor is a nonzerodivisor of Γ(X, U) with Γ(X, U) ⧸ (a) flat over Γ(S, W). For an affine open V of T over W, it therefore stays a nonzerodivisor in Γ(X, U) ⊗[Γ(S, W)] Γ(T, V) (Module.Flat.isSMulRegular_one_tmul_of_quotient_span_singleton). There it is a local equation of the pulled-back divisor on the open subscheme Spec (Γ(X, U) ⊗[Γ(S, W)] Γ(T, V)) of X ×_S T.

Main results

• Scheme.IdealSheafData.IsRelativeEffectiveCartier: an effective Cartier divisor flat over the base.
• Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap_iff: after arbitrary base change, relativity reduces to the effective Cartier condition on the pulled-back ideal.
• Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap: a relative effective Cartier divisor remains one after an arbitrary base change.
• Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap_of_flat: it also remains one after pullback along a flat morphism X' ⟶ X, relative to the composite X' ⟶ S.
• Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap_of_isPullback: base change along any pullback square, not only along the chosen fibre product X ×_S T.
• Scheme.IdealSheafData.isRelativeEffectiveCartier_top: the empty divisor is relative effective Cartier over every base.
• Scheme.IdealSheafData.isRelativeEffectiveCartier_iff_isEffectiveCartier: over the spectrum of a field, every effective Cartier divisor is relative effective Cartier.

References

• Stacks Project, Divisors, Relative effective Cartier divisors (stability under base change).

def AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier {S X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) : Prop

An effective Cartier divisor relative to S is an effective Cartier divisor whose closed subscheme is flat over S.

Equations

• I.IsRelativeEffectiveCartier f = (I.IsEffectiveCartier ∧ AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f))

theorem AlgebraicGeometry.Scheme.IdealSheafData.isRelativeEffectiveCartier_iff {S X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) : I.IsRelativeEffectiveCartier f ↔ I.IsEffectiveCartier ∧ Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f)

A divisor is relative effective Cartier exactly when it is effective Cartier and its closed subscheme is flat over the base.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isEffectiveCartier {S X : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) : I.IsEffectiveCartier

A relative effective Cartier divisor is an effective Cartier divisor on its ambient scheme.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.flat {S X : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) : Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f)

The closed subscheme of a relative effective Cartier divisor is flat over the base.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap_iff {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) [Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f)] : (I.comap (CategoryTheory.Limits.pullback.fst f g)).IsRelativeEffectiveCartier (CategoryTheory.Limits.pullback.snd f g) ↔ (I.comap (CategoryTheory.Limits.pullback.fst f g)).IsEffectiveCartier

If the original closed subscheme is flat over the base, its arbitrary base change is relative effective Cartier if and only if the pulled-back ideal is effective Cartier.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap {S T X : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) (g : T ⟶ S) : (I.comap (CategoryTheory.Limits.pullback.fst f g)).IsRelativeEffectiveCartier (CategoryTheory.Limits.pullback.snd f g)

Relative effective Cartier divisors are stable under arbitrary base change. If I is a relative effective Cartier divisor on X over S, then for every morphism g : T ⟶ S its pullback to X ×_S T is a relative effective Cartier divisor over T. Neither g nor X ⟶ S need be flat.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap_of_flat {S X X' : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) (g : X' ⟶ X) [Flat g] : (I.comap g).IsRelativeEffectiveCartier (CategoryTheory.CategoryStruct.comp g f)

Flat pullback of relative effective Cartier divisors. If I is a relative effective Cartier divisor on X over S and g : X' ⟶ X is flat, then the pullback of I to X' is a relative effective Cartier divisor over S through g ≫ f.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.comap_of_isPullback {S T X X' : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) {g : T ⟶ S} {g' : X' ⟶ X} {f' : X' ⟶ T} (h : CategoryTheory.IsPullback g' f' f g) : (I.comap g').IsRelativeEffectiveCartier f'

Relative effective Cartier divisors are stable under base change along a pullback square. Given a pullback square with g' : X' ⟶ X over g : T ⟶ S, the pullback along g' of a relative effective Cartier divisor on X over S is a relative effective Cartier divisor on X' over T.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.isRelativeEffectiveCartier_top {S X : Scheme} (f : X ⟶ S) : ⊤.IsRelativeEffectiveCartier f

The empty closed subscheme is a relative effective Cartier divisor over every base.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.isRelativeEffectiveCartier_iff_isEffectiveCartier {S X : Scheme} [Subsingleton ↥S] [IsIntegral S] (I : X.IdealSheafData) (f : X ⟶ S) : I.IsRelativeEffectiveCartier f ↔ I.IsEffectiveCartier

Over the spectrum of a field, flatness over the base is automatic, so the relative effective Cartier divisors are exactly the effective Cartier divisors.