Regular proper and projective curves are anti-equivalent to algebraic function fields #
Let k be a field. This file proves that the function-field functor
X ↦ k(X) from regular proper curves over k (with dominant k-morphisms) to algebraic
function fields of one variable over k (with k-embeddings) is an anti-equivalence of
categories. Its inverse is the model functor: a function field F goes to its two-chart
model, the normalization of the projective line in F glued from the normalizations of k[x]
and k[x⁻¹] for a transcendental x ∈ F chosen once and for all, and a k-embedding
φ : F → F' goes to the unique dominant k-morphism of models whose pullback of rational functions
is φ (TauCeti.AlgebraicGeometry.twoChartModel.homOfAlgHom).
The two natural isomorphisms are the ones already constructed object by object:
- the function field of the model of
FisF(TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv), naturally inFbecause the pullback alonghomOfAlgHom φisφ; - a regular proper curve
Xis the model of its function field (AlgebraicGeometry.Scheme.isoTwoChartModel), naturally inXbecause a dominantk-morphism into a separated scheme is determined by its pullback of rational functions.
Every regular proper curve is projective
(AlgebraicGeometry.Scheme.isProjectiveOver_of_isCurveOver), so the regular projective curves, a
full subcategory of the regular proper curves, are all of them. The anti-equivalence therefore also
holds with regular projective curves on the geometric side, as in Hartshorne's Corollary I.6.12.
Main definitions #
TauCeti.AlgebraicGeometry.RegularProperCurveCat.twoChartModelFunctor: the model functorF ↦ twoChartModel F.TauCeti.AlgebraicGeometry.RegularProperCurveCat.twoChartModelFunctorCompFunctionFieldFunctorIso: the function field of the model ofFisF, naturally inF.RegularProperCurveCat.idIsoFunctionFieldFunctorCompTwoChartModelFunctor: a regular proper curve is the model of its function field, naturally in the curve.TauCeti.AlgebraicGeometry.RegularProperCurveCat.equivFunctionFieldCat: the anti-equivalenceRegularProperCurveCat k ≌ (FunctionFieldCat k)ᵒᵖ, with functor the function-field functor, inverse the model functor, and the two natural isomorphisms above as counit and unit.TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.equivRegularProperCurveCat: regarding a regular projective curve as a regular proper curve is an equivalence of categories.TauCeti.AlgebraicGeometry.RegularProjectiveCurveCat.equivFunctionFieldCat: the anti-equivalenceRegularProjectiveCurveCat k ≌ (FunctionFieldCat k)ᵒᵖbetween regular projective curves and algebraic function fields.
Main results #
- the instances
(functionFieldFunctor k).IsEquivalence,(twoChartModelFunctor k).IsEquivalenceand(RegularProjectiveCurveCat.toRegularProperCurveCat k).IsEquivalence.
References #
- R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Corollary I.6.12.
- Q. Liu, Algebraic Geometry and Arithmetic Curves, Oxford GTM 6, 2002, Section 7.3.
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Appendix B.
The transcendental function of F from which the model of F is built.
Instances For
The function modelGenerator F is transcendental over k.
The function modelGenerator F is nonzero.
The private abbreviations modelObj and modelHom below are the object and morphism parts
of twoChartModelFunctor, whose obj and map fields are the same terms, so the two agree by
rfl. The unit, the counit and their naturality proofs go through these abbreviations because
they are reducible: instance search sees the k-algebra and over-k instances of
twoChartModel through them, but does not unfold the fields of the functor. Being private, they
cannot appear in the exposed body of twoChartModelFunctor itself.
The model functor: the contravariant functor from algebraic function fields over k to
regular proper curves over k sending F to its two-chart model (the normalization of the
projective line in F) and a k-embedding φ : F → F' to the unique dominant k-morphism of
models whose pullback of rational functions is φ.
Instances For
The model functor sends F to the two-chart model of F built from modelGenerator F.
The model functor sends a k-embedding φ to the morphism of two-chart models induced
by φ.
The pullback of rational functions along the morphism of models induced by φ : G → F is
φ, read through the identifications of the function fields of the models with G and F.
The function field of the model of F is F, naturally in F.
Instances For
The component at F of the natural isomorphism
twoChartModelFunctorCompFunctionFieldFunctorIso is the identification of F with the function
field of its model.
The inverse component at F of the natural isomorphism
twoChartModelFunctorCompFunctionFieldFunctorIso is the identification of the function field of
the model of F with F.
A regular proper curve is the model of its function field, naturally in the curve.
Instances For
The component at X of the natural isomorphism
idIsoFunctionFieldFunctorCompTwoChartModelFunctor is the isomorphism of X with the two-chart
model of its function field.
The inverse component at X of the natural isomorphism
idIsoFunctionFieldFunctorCompTwoChartModelFunctor is the isomorphism of the two-chart model of
the function field of X with X.
The triangle law for the unit idIsoFunctionFieldFunctorCompTwoChartModelFunctor and the
counit twoChartModelFunctorCompFunctionFieldFunctorIso.
The anti-equivalence between regular proper curves and algebraic function fields over a
field k: the function-field functor X ↦ k(X) is an equivalence
RegularProperCurveCat k ≌ (FunctionFieldCat k)ᵒᵖ with inverse the model functor
F ↦ twoChartModel F.
Instances For
A regular proper curve, as a regular projective curve: it is projective over k by
AlgebraicGeometry.Scheme.isProjectiveOver_of_isCurveOver.
Instances For
Regular projective curves are regular proper curves: regarding a regular projective curve as a regular proper curve is an equivalence of categories, because every regular proper curve is projective.
Instances For
The anti-equivalence between regular projective curves and algebraic function fields over
a field k: the functor sending a regular projective curve X to its function field k(X) and a
dominant k-morphism to the pullback of rational functions along it is an equivalence
RegularProjectiveCurveCat k ≌ (FunctionFieldCat k)ᵒᵖ. Its inverse sends a function field to its
two-chart model, the normalization of the projective line in it.
Instances For
The anti-equivalence sends a regular projective curve to its function field.
The anti-equivalence sends a dominant k-morphism to the pullback of rational functions
along it.
The inverse of the anti-equivalence sends a function field F to the two-chart model of F
built from modelGenerator F.
The inverse of the anti-equivalence sends a k-embedding of function fields to the induced
dominant k-morphism of two-chart models.
The unit of the anti-equivalence at X is the isomorphism of X with the two-chart model of
its function field.
The inverse of the unit of the anti-equivalence at X is the isomorphism of the two-chart
model of the function field of X with X.
The counit of the anti-equivalence at F identifies the function field of the two-chart model
of F with F.
The inverse of the counit of the anti-equivalence at F identifies F with the function
field of the two-chart model of F.