Prestable families of curves

A prestable family is a proper nodal relative curve with geometrically connected fibres. Nodality is the scheme-theoretic criterion of syntomicity of relative dimension one and unramifiedness of the relative singular subscheme. In particular, the fibres have pure dimension one. No genus bound or projectivity hypothesis is part of this notion.

Prestable families are families of curves. They are invariant under isomorphisms, local on the base, and stable under arbitrary base change; thus their restrictions and fibres are again prestable. Smooth proper geometrically connected relative curves provide examples.

Over a local domain of Krull dimension at most one, for instance a discrete valuation ring, a morphism is a prestable family exactly when it is proper, flat and locally of finite presentation and its generic and special fibres are prestable curves (TauCeti.AlgebraicGeometry.prestableFamily_iff_genericFiber_and_specialFiber).

References

• The Stacks Project, Section 109.20, Prestable curves

class TauCeti.AlgebraicGeometry.PrestableFamily {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) extends AlgebraicGeometry.IsProper f, AlgebraicGeometry.GeometricallyConnected f : Prop

A prestable family is a proper at-worst-nodal relative curve with geometrically connected fibres. Its genus is separate data; in particular genus zero is allowed.

• isClosedImmersion_diagonal : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
• universally_isClosedMap : (topologically @IsClosedMap).universally f
• finiteType_appLE {U : S.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType
• geometrically_connectedSpace : geometrically (fun (x : Scheme) => ConnectedSpace ↥x) f
• atWorstNodalOfRelativeDimensionOne : AtWorstNodalOfRelativeDimensionOne f

  The family is nodal, including at its smooth points.

theorem TauCeti.AlgebraicGeometry.prestableFamily_iff {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : PrestableFamily f ↔ AlgebraicGeometry.IsProper f ∧ AlgebraicGeometry.GeometricallyConnected f ∧ AtWorstNodalOfRelativeDimensionOne f

instance TauCeti.AlgebraicGeometry.PrestableFamily.syntomic {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [PrestableFamily f] : SyntomicOfRelativeDimension 1 f

A prestable family is syntomic of relative dimension one.

instance TauCeti.AlgebraicGeometry.PrestableFamily.familyOfCurves {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [PrestableFamily f] : FamilyOfCurves f

A prestable family is a family of curves: it is proper, flat, finitely presented, and has relative dimension at most one.

instance TauCeti.AlgebraicGeometry.PrestableFamily.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @PrestableFamily

Prestable families are stable under arbitrary base change.

instance TauCeti.AlgebraicGeometry.PrestableFamily.respectsIso : CategoryTheory.MorphismProperty.RespectsIso @PrestableFamily

Prestable families are invariant under isomorphisms of arrows.

instance TauCeti.AlgebraicGeometry.PrestableFamily.isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @PrestableFamily

Being prestable is local on the base for the Zariski topology.

theorem TauCeti.AlgebraicGeometry.PrestableFamily.of_isPullback {X Y Z P : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [PrestableFamily f] : PrestableFamily snd

An arbitrary pullback of a prestable family is prestable.

instance TauCeti.AlgebraicGeometry.PrestableFamily.pullback_snd {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [PrestableFamily f] : PrestableFamily (CategoryTheory.Limits.pullback.snd f g)

The base change of a prestable family along any morphism is prestable.

instance TauCeti.AlgebraicGeometry.PrestableFamily.pullback_fst {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [PrestableFamily g] : PrestableFamily (CategoryTheory.Limits.pullback.fst f g)

The base change of a prestable family along any morphism is prestable.

instance TauCeti.AlgebraicGeometry.PrestableFamily.morphismRestrict {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (U : S.Opens) [PrestableFamily f] : PrestableFamily (f ∣_ U)

Restricting a prestable family to an open subscheme of the base preserves prestability.

instance TauCeti.AlgebraicGeometry.PrestableFamily.fiberToSpecResidueField {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [PrestableFamily f] : PrestableFamily (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f s)

Every residue-field fibre of a prestable family is a prestable curve.

theorem TauCeti.AlgebraicGeometry.PrestableFamily.of_smooth {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.GeometricallyConnected f] : PrestableFamily f

A smooth proper relative curve of pure relative dimension one with geometrically connected fibres is prestable.

theorem TauCeti.AlgebraicGeometry.prestableFamily_iff_genericFiber_and_specialFiber {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [IsLocalRing ↑R] [IsDomain ↑R] [Ring.DimensionLEOne ↑R] (K : Type u) [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] (toBase : X ⟶ AlgebraicGeometry.Spec R) : PrestableFamily toBase ↔ AlgebraicGeometry.IsProper toBase ∧ AlgebraicGeometry.Flat toBase ∧ AlgebraicGeometry.LocallyOfFinitePresentation toBase ∧ PrestableFamily (genericFiber (↑R) K toBase).hom ∧ PrestableFamily (specialFiber (↑R) toBase).hom

The two-fibre criterion for prestable families. Over a local domain of dimension at most one, for instance a discrete valuation ring, a morphism is a prestable family exactly when it is proper, flat and locally of finite presentation and both its generic fibre over the fraction field and its special fibre over the residue field are prestable curves.