The two-chart model is a curve

The two-chart model of an algebraic function field is an example of a proper integral curve. Over a perfect field it is moreover smooth of relative dimension one (TauCeti.AlgebraicGeometry.twoChartModel.smoothOfRelativeDimension_one_of_perfectField), being a regular curve.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isCurveOver {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : AlgebraicGeometry.Scheme.IsCurveOver k

The two-chart model of a function field is a proper integral curve with that function field.

theorem TauCeti.AlgebraicGeometry.twoChartModel.smoothOfRelativeDimension_one_of_perfectField {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} [PerfectField k] (hxt : Transcendental k x) : AlgebraicGeometry.SmoothOfRelativeDimension 1 (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k)

Over a perfect field the two-chart model is smooth of relative dimension one, for x transcendental over k: it is a regular curve.