Families of curves

A morphism of schemes f : X ⟶ S is a family of curves if it is proper, flat, of finite presentation, and of relative dimension at most one, following the Stacks Project's notion of a family of curves over a scheme base. Nodal, prestable, semistable, and stable families of curves are families of curves satisfying further conditions. Geometric connectedness of the fibres and the genus are deliberately not part of the definition.

Finite presentation is recorded as LocallyOfFinitePresentation: a proper morphism is already quasi-compact and separated, hence quasi-separated.

The notion is invariant under isomorphisms, local on the target, and stable under arbitrary base change. Over a field, it says that a proper scheme has dimension at most one. Finite flat morphisms of finite presentation are families of curves.

Main declarations

• TauCeti.AlgebraicGeometry.FamilyOfCurves f: f is a family of curves.
• TauCeti.AlgebraicGeometry.FamilyOfCurves.isZariskiLocalAtTarget: locality on the target.
• TauCeti.AlgebraicGeometry.FamilyOfCurves.of_isPullback: stability under base change.
• TauCeti.AlgebraicGeometry.familyOfCurves_iff_of_field: families of curves over a field.

References

• Stacks Project, Tag 0D4Z

class TauCeti.AlgebraicGeometry.FamilyOfCurves {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) extends AlgebraicGeometry.IsProper f, AlgebraicGeometry.Flat f, AlgebraicGeometry.LocallyOfFinitePresentation f, TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f : Prop

A morphism of schemes f : X ⟶ S is a family of curves if it is proper, flat, locally of finite presentation, and of relative dimension at most one. Being proper, such a morphism is quasi-compact and quasi-separated, hence of finite presentation.

• 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
• flat_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)).Flat
• finitePresentation_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)).FinitePresentation
• topologicalKrullDim_fiber_le (y : ↥S) : topologicalKrullDim ↥(AlgebraicGeometry.Scheme.Hom.fiber f y) ≤ ↑1

theorem TauCeti.AlgebraicGeometry.familyOfCurves_iff {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) : FamilyOfCurves f ↔ AlgebraicGeometry.IsProper f ∧ AlgebraicGeometry.Flat f ∧ AlgebraicGeometry.LocallyOfFinitePresentation f ∧ RelativeDimensionLE 1 f

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

Being a family of curves is invariant under isomorphisms of arrows.

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

The restriction of a family of curves to an open subscheme of the base is a family of curves.

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

Being a family of curves is local on the target.

theorem TauCeti.AlgebraicGeometry.FamilyOfCurves.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) [FamilyOfCurves f] : FamilyOfCurves snd

Being a family of curves is stable under arbitrary base change.

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

Being a family of curves is stable under arbitrary base change.

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

The base change pullback.snd f g of a family of curves f is a family of curves.

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

The base change pullback.fst f g of a family of curves g is a family of curves.

@[instance 100]

instance TauCeti.AlgebraicGeometry.FamilyOfCurves.of_isFinite {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f] [AlgebraicGeometry.Flat f] [AlgebraicGeometry.LocallyOfFinitePresentation f] : FamilyOfCurves f

A finite flat morphism of finite presentation is a family of curves.

theorem TauCeti.AlgebraicGeometry.familyOfCurves_iff_of_field {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] (f : X ⟶ AlgebraicGeometry.Spec ↧K) : FamilyOfCurves f ↔ AlgebraicGeometry.IsProper f ∧ topologicalKrullDim ↥X ≤ 1

A scheme over a field is a family of curves over it if and only if it is proper and of Krull dimension at most one.