Relative effective Cartier divisors of fixed degree

Let f : X ⟶ S be a proper family of curves. A relative effective Cartier divisor D on X_T = T ×_S X is finite flat over T, so its degree at t : T is the rank of its closed subscheme over t. The degree is preserved by arbitrary base change. Consequently, the divisors whose degree is everywhere a fixed natural number d form a subfunctor Div^d_{X/S} of the functor of relative effective Cartier divisors.

This fixed-degree functor is the functor represented by the symmetric power Symᵈ X when f is a smooth proper curve. This file constructs the functor; it does not prove representability.

Main declarations

• TauCeti.AlgebraicGeometry.relativeEffectiveCartierDegreeSubfunctor: the subfunctor Div^d_{X/S} of relative effective Cartier divisors of degree d;
• TauCeti.AlgebraicGeometry.relativeEffectiveCartierDegreeOneSection: the degree-one divisor supplied by a section of a smooth proper relative curve.

References

• S. Kleiman, The Picard scheme, in Fundamental Algebraic Geometry: Grothendieck's FGA Explained, Section 9.3.
• The Stacks Project, Picard Schemes of Curves, section Moduli of divisors on smooth curves.

def TauCeti.AlgebraicGeometry.relativeEffectiveCartierDegreeSubfunctor {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [RelativeDimensionLE 1 f] (d : ℕ) : CategoryTheory.Subfunctor (relativeEffectiveCartierSubfunctor f).toFunctor

The subfunctor Div^d_{X/S} of relative effective Cartier divisors of degree d.

At an S-scheme T, its elements are relative effective Cartier divisors on X_T = T ×_S X whose finite flat closed subscheme has rank d at every point of T. Arbitrary base change preserves this condition.

@[simp]

theorem TauCeti.AlgebraicGeometry.mem_relativeEffectiveCartierDegreeSubfunctor_obj_iff {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [RelativeDimensionLE 1 f] {d : ℕ} {T : (CategoryTheory.Over S)ᵒᵖ} {D : (relativeEffectiveCartierSubfunctor f).toFunctor.obj T} : D ∈ (relativeEffectiveCartierDegreeSubfunctor f d).obj T ↔ AlgebraicGeometry.Scheme.Hom.finrank (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.subschemeι ↑D) (CategoryTheory.Limits.pullback.fst (Opposite.unop T).hom f)) = fun (x : ↥(Opposite.unop T).left) => d

A relative effective Cartier divisor belongs to Div^d_{X/S} exactly when the rank of its closed subscheme over the base is constantly d.

noncomputable def TauCeti.AlgebraicGeometry.relativeEffectiveCartierDegreeOneSection {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [RelativeDimensionLE 1 f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : (relativeEffectiveCartierDegreeSubfunctor f 1).toFunctor.obj T

The degree-one relative effective Cartier divisor obtained by pulling a fixed section x₀ back to X_T for every S-scheme T.

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeEffectiveCartierDegreeOneSection_val {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [RelativeDimensionLE 1 f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) (T : (CategoryTheory.Over S)ᵒᵖ) : ↑↑(relativeEffectiveCartierDegreeOneSection f x₀ hx₀ T) = AlgebraicGeometry.Scheme.Hom.ker (baseChangeSection f x₀ hx₀ (Opposite.unop T))

The ideal sheaf underlying the degree-one divisor supplied by a section is the kernel of the base-changed section.

theorem TauCeti.AlgebraicGeometry.relativeEffectiveCartierDegreeOneSection_map {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [RelativeDimensionLE 1 f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (x₀ : S ⟶ X) (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) : (CategoryTheory.ConcreteCategory.hom ((relativeEffectiveCartierDegreeSubfunctor f 1).toFunctor.map φ)) (relativeEffectiveCartierDegreeOneSection f x₀ hx₀ T) = relativeEffectiveCartierDegreeOneSection f x₀ hx₀ T'

Pulling back the degree-one divisor supplied by x₀ gives the divisor supplied by the base-changed section.