The category of regular proper curves and the function-field functor

A regular proper curve over a field k is a curve over k (an integral scheme, proper and of dimension one over k) whose local rings at its codimension-one points, its closed points, are discrete valuation rings. With the dominant k-morphisms as morphisms these curves form a category, the geometric side of the anti-equivalence with algebraic function fields of one variable over k.

Taking function fields is a contravariant functor from this category to the category TauCeti.FunctionFieldCat k of algebraic function fields over k: a curve goes to its function field k(X), an algebraic function field by AlgebraicGeometry.Scheme.IsCurveOver.isFunctionField, and a dominant k-morphism f : X ⟶ Y to the pullback of rational functions f^* : k(Y) → k(X), a k-algebra homomorphism by AlgebraicGeometry.Scheme.Hom.functionFieldAlgHom.

A regular projective curve over k is an integral scheme of dimension one, projective over k in the sense of AlgebraicGeometry.Scheme.IsProjectiveOver, whose local rings at its codimension-one points are discrete valuation rings. A projective scheme is proper, so a regular projective curve is a regular proper curve, and the regular projective curves form a full subcategory of the regular proper curves. Every regular proper curve is projective (AlgebraicGeometry.Scheme.isProjectiveOver_of_isCurveOver), so this inclusion is an equivalence (TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.equivRegularProperCurveCat).

Main definitions

• TauCeti.AlgebraicGeometry.RegularProperCurveCat k: the category of regular proper curves over k with dominant k-morphisms.
• TauCeti.AlgebraicGeometry.RegularProperCurveCat.isoMk: an isomorphism of regular proper curves from an isomorphism of schemes over k.
• TauCeti.AlgebraicGeometry.RegularProperCurveCat.functionFieldFunctor: the contravariant function-field functor X ↦ k(X).
• TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat k: the category of regular projective curves over k with dominant k-morphisms.
• TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.toRegularProperCurveCat: the fully faithful functor regarding a regular projective curve as a regular proper curve.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section I.6.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Appendix B.

structure TauCeti.AlgebraicGeometry.RegularProperCurveCat (k : Type u) [Field k] : Type (u + 1)

The category of regular proper curves over a field k: curves over k (integral schemes, proper and of dimension one over k) whose local rings at the codimension-one points are discrete valuation rings, with the dominant k-morphisms as morphisms.

• toScheme : AlgebraicGeometry.Scheme

  The underlying scheme.

• over : self.toScheme.Over (AlgebraicGeometry.Spec ↧k)
• isCurveOver : AlgebraicGeometry.Scheme.IsCurveOver k
• isDiscreteValuationRing_stalk (y : CodimensionOnePoint self.toScheme) : IsDiscreteValuationRing ↑(self.toScheme.presheaf.stalk ↑y)

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.RegularProperCurveCat.of {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.Scheme.IsCurveOver k] [∀ (y : CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] : RegularProperCurveCat k

The object of RegularProperCurveCat k given by a curve over k whose local rings at the codimension-one points are discrete valuation rings.

structure TauCeti.AlgebraicGeometry.RegularProperCurveCat.Hom {k : Type u} [Field k] (X Y : RegularProperCurveCat k) : Type u

The type of morphisms in RegularProperCurveCat k: the dominant k-morphisms of schemes.

• hom : X.toScheme ⟶ Y.toScheme

  The underlying morphism of schemes.

• isOver : AlgebraicGeometry.Scheme.Hom.IsOver self.hom (AlgebraicGeometry.Spec ↧k)
• isDominant : AlgebraicGeometry.IsDominant self.hom

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.Hom.ext {k : Type u} {inst✝ : Field k} {X Y : RegularProperCurveCat k} {x y : X.Hom Y} (hom : x.hom = y.hom) : x = y

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.Hom.ext_iff {k : Type u} {inst✝ : Field k} {X Y : RegularProperCurveCat k} {x y : X.Hom Y} : x = y ↔ x.hom = y.hom

@[instance_reducible]

instance TauCeti.AlgebraicGeometry.RegularProperCurveCat.instCategory {k : Type u} [Field k] : CategoryTheory.Category.{u, u + 1} (RegularProperCurveCat k)

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.id_hom {k : Type u} [Field k] (X : RegularProperCurveCat k) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.toScheme

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.comp_hom {k : Type u} [Field k] {X Y Z : RegularProperCurveCat k} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.hom_ext {k : Type u} [Field k] {X Y : RegularProperCurveCat k} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.hom_ext_iff {k : Type u} [Field k] {X Y : RegularProperCurveCat k} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

def TauCeti.AlgebraicGeometry.RegularProperCurveCat.isoMk {k : Type u} [Field k] {X Y : RegularProperCurveCat k} (e : X.toScheme ≅ Y.toScheme) [AlgebraicGeometry.Scheme.Hom.IsOver e.hom (AlgebraicGeometry.Spec ↧k)] : X ≅ Y

An isomorphism of regular proper curves over k from an isomorphism of the underlying schemes over k.

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.isoMk_hom_hom {k : Type u} [Field k] {X Y : RegularProperCurveCat k} (e : X.toScheme ≅ Y.toScheme) [AlgebraicGeometry.Scheme.Hom.IsOver e.hom (AlgebraicGeometry.Spec ↧k)] : (isoMk e).hom.hom = e.hom

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.isoMk_inv_hom {k : Type u} [Field k] {X Y : RegularProperCurveCat k} (e : X.toScheme ≅ Y.toScheme) [AlgebraicGeometry.Scheme.Hom.IsOver e.hom (AlgebraicGeometry.Spec ↧k)] : (isoMk e).inv.hom = e.inv

noncomputable def TauCeti.AlgebraicGeometry.RegularProperCurveCat.functionFieldFunctor (k : Type u) [Field k] : CategoryTheory.Functor (RegularProperCurveCat k) (FunctionFieldCat k)ᵒᵖ

The function-field functor: the contravariant functor from regular proper curves over k to algebraic function fields over k sending a curve X to its function field k(X) and a dominant k-morphism f : X ⟶ Y to the pullback of rational functions f^* : k(Y) → k(X).

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.functionFieldFunctor_obj (k : Type u) [Field k] (X : RegularProperCurveCat k) : (functionFieldFunctor k).obj X = Opposite.op (FunctionFieldCat.of ↑X.toScheme.functionField ⋯)

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProperCurveCat.functionFieldFunctor_map_unop_hom {k : Type u} [Field k] {X Y : RegularProperCurveCat k} (f : X ⟶ Y) : FunctionFieldCat.Hom.hom ((functionFieldFunctor k).map f).unop = AlgebraicGeometry.Scheme.Hom.functionFieldAlgHom k f.hom

The function-field functor sends a dominant k-morphism to the pullback of rational functions along it.

structure TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat (k : Type u) [Field k] : Type (u + 1)

The category of regular projective curves over a field k: integral schemes of dimension one, projective over k, whose local rings at the codimension-one points are discrete valuation rings, with the dominant k-morphisms as morphisms.

• toScheme : AlgebraicGeometry.Scheme

  The underlying scheme.

• over : self.toScheme.Over (AlgebraicGeometry.Spec ↧k)
• isIntegral : AlgebraicGeometry.IsIntegral self.toScheme
• isProjectiveOver : AlgebraicGeometry.Scheme.IsProjectiveOver k
• topologicalKrullDim_eq_one : topologicalKrullDim ↥self.toScheme = 1

  The curve has dimension one.

• isDiscreteValuationRing_stalk (y : CodimensionOnePoint self.toScheme) : IsDiscreteValuationRing ↑(self.toScheme.presheaf.stalk ↑y)

instance TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.isCurveOver {k : Type u} [Field k] (X : RegularProjectiveCurveCat k) : AlgebraicGeometry.Scheme.IsCurveOver k

A regular projective curve is a curve: projective schemes are proper.

@[instance_reducible]

instance TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.instCategory {k : Type u} [Field k] : CategoryTheory.Category.{u, u + 1} (RegularProjectiveCurveCat k)

Regular projective curves over k form a category, with the dominant k-morphisms of the underlying regular proper curves as morphisms.

def TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.toRegularProperCurveCat (k : Type u) [Field k] : CategoryTheory.Functor (RegularProjectiveCurveCat k) (RegularProperCurveCat k)

The functor regarding a regular projective curve as a regular proper curve. It is fully faithful (RegularProjectiveCurveCat.fullyFaithfulToRegularProperCurveCat) and an equivalence, since every regular proper curve is projective (RegularProjectiveCurveCat.equivRegularProperCurveCat).

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.toRegularProperCurveCat_obj_toScheme {k : Type u} [Field k] (X : RegularProjectiveCurveCat k) : ((toRegularProperCurveCat k).obj X).toScheme = X.toScheme

@[simp]

theorem TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.toRegularProperCurveCat_map {k : Type u} [Field k] {X Y : RegularProjectiveCurveCat k} (f : X ⟶ Y) : (toRegularProperCurveCat k).map f = f.hom

def TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.fullyFaithfulToRegularProperCurveCat (k : Type u) [Field k] : (toRegularProperCurveCat k).FullyFaithful

The functor regarding a regular projective curve as a regular proper curve is fully faithful.

instance TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.instFullRegularProperCurveCatToRegularProperCurveCat {k : Type u} [Field k] : (toRegularProperCurveCat k).Full

instance TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.instFaithfulRegularProperCurveCatToRegularProperCurveCat {k : Type u} [Field k] : (toRegularProperCurveCat k).Faithful