Two affine opens covering a regular proper curve

A regular proper integral curve over a field is covered by two affine opens. Indeed, a transcendental rational function identifies the curve with the two-chart model of its function field, and the two normalization charts pull back to the required opens.

The result is also stated directly for smooth proper connected curves of relative dimension one. It requires neither a rational point nor a perfect base field. The cover is the geometric input for computing quasi-coherent cohomology by the two-open Mayer–Vietoris sequence; the intersection is affine because a proper curve is separated.

The construction uses Scheme.isoTwoChartModel and the two affine charts of twoChartModel.

References

• R. Hartshorne, Algebraic Geometry, Chapter I, Theorem 6.9 and Corollary 6.12 (proper nonsingular curves and their function fields).

theorem AlgebraicGeometry.Scheme.exists_two_affine_opens {k : Type u} [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsCurveOver k] [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X), IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)] : ∃ (U : X.Opens) (V : X.Opens), IsAffineOpen U ∧ IsAffineOpen V ∧ U ⊔ V = ⊤

A proper integral curve whose codimension-one local rings are discrete valuation rings is covered by two affine open subsets.

theorem AlgebraicGeometry.Scheme.exists_two_affine_opens_of_smooth {k : Type u} [Field k] (X : Scheme) [X.Over (Spec ↧k)] [IsProper (X ↘ Spec ↧k)] [SmoothOfRelativeDimension 1 (X ↘ Spec ↧k)] [ConnectedSpace ↥X] : ∃ (U : X.Opens) (V : X.Opens), IsAffineOpen U ∧ IsAffineOpen V ∧ U ⊔ V = ⊤

A smooth proper connected curve over any field admits a cover by two affine open subsets, without a rational-point hypothesis.