The projective line as a model of the projective line

Let R be a discrete valuation ring with fraction field K. The projective line ℙ¹_R is a smooth proper model over R of the projective line ℙ¹_K: its generic fibre is ℙ¹_K, since the formation of ℙ¹ commutes with base change (TauCeti.AlgebraicGeometry.projectiveLine.isPullback_baseChangeProjection).

Main definitions

• TauCeti.Model.projectiveLine R K: the projective line ℙ¹_R, as a model of ℙ¹_K over R.

Main results

• TauCeti.Model.smoothOfRelativeDimension_projectiveLine and TauCeti.Model.isProper_projectiveLine: this model is smooth of relative dimension one and proper.

References

• Q. Liu, Algebraic Geometry and Arithmetic Curves, Oxford University Press, 2002, Section 10.1: models of curves.

noncomputable def TauCeti.Model.projectiveLineGenericFiberIso (R K : Type u) [CommRing R] [Field K] [Algebra R K] : genericFiber R K (AlgebraicGeometry.projectiveLine R ↘ AlgebraicGeometry.Spec ↧R) ≅ CategoryTheory.Over.mk (AlgebraicGeometry.projectiveLine K ↘ AlgebraicGeometry.Spec ↧K)

The identification of the generic fibre of ℙ¹_R with ℙ¹_K, over K.

noncomputable def TauCeti.Model.projectiveLine (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : Model R K (AlgebraicGeometry.projectiveLine K) (AlgebraicGeometry.projectiveLine K ↘ AlgebraicGeometry.Spec ↧K)

The projective line ℙ¹_R as a model of ℙ¹_K: its generic fibre is identified with ℙ¹_K through the base change of the projective line along R → K.

theorem TauCeti.Model.projectiveLineGenericFiberIso_inv_left (R K : Type u) [CommRing R] [Field K] [Algebra R K] : CategoryTheory.Over.Hom.left (projectiveLineGenericFiberIso R K).inv = ⋯.isoPullback.hom

The inverse of the generic-fibre identification is the canonical pullback isomorphism.

@[simp]

theorem TauCeti.Model.projectiveLine_total (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : (projectiveLine R K).total = AlgebraicGeometry.projectiveLine R

The total space of the model ℙ¹_R is the projective line over R.

@[simp]

theorem TauCeti.Model.projectiveLine_toBase (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : (projectiveLine R K).toBase = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.projectiveLine R ↘ AlgebraicGeometry.Spec ↧R)

The structure morphism of the model ℙ¹_R is that of the projective line over R.

@[simp]

theorem TauCeti.Model.genericι_projectiveLine (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : (projectiveLine R K).genericι = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.projectiveLine.baseChangeProjection R K) (CategoryTheory.eqToHom ⋯)

The generic fibre of the projective-line model is included by base-change projection.

instance TauCeti.Model.smoothOfRelativeDimension_projectiveLine (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : AlgebraicGeometry.SmoothOfRelativeDimension 1 (projectiveLine R K).toBase

The model ℙ¹_R of ℙ¹_K is smooth of relative dimension one over R.

theorem TauCeti.Model.isProper_projectiveLine (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : (projectiveLine R K).IsProper

The model ℙ¹_R of ℙ¹_K is proper over R.