The two-chart model of a function field is separated

Let F / k be an algebraic function field and x ∈ F nonzero. The scheme TauCeti.AlgebraicGeometry.twoChartModel hF hx is glued from the affine charts Spec 𝒪_x and Spec 𝒪_{x⁻¹} along Spec 𝒪_{x, x⁻¹}, where 𝒪_x, 𝒪_{x⁻¹} and 𝒪_{x, x⁻¹} are the holomorphy rings of the places at which x, x⁻¹, and both are regular. This file proves that it is a separated scheme.

The two charts meet exactly in Spec 𝒪_{x, x⁻¹} (TauCeti.AlgebraicGeometry.twoChartModel.isPullback), so by the gluing criterion AlgebraicGeometry.IsSeparated.pushout_desc_iff it suffices that Spec 𝒪_{x, x⁻¹} is a closed subscheme of Spec (𝒪_x ⊗_k 𝒪_{x⁻¹}), that is, that 𝒪_x ⊗_k 𝒪_{x⁻¹} → 𝒪_{x, x⁻¹} is surjective. It is: 𝒪_{x, x⁻¹} is the localization of 𝒪_x away from x (TauCeti.exists_pow_mul_mem_holomorphyRing), so every z ∈ 𝒪_{x, x⁻¹} is (xⁿ z) · (x⁻¹)ⁿ with xⁿ z ∈ 𝒪_x and (x⁻¹)ⁿ ∈ 𝒪_{x⁻¹}. This is the argument that shows the projective line, glued from Spec k[x] and Spec k[x⁻¹], is separated.

Separatedness is one of the properties of the normalization of the projective line in F, and it is the hypothesis under which the codimension-one points of a curve are determined by their places (CodimensionOnePoint.toPlace_injective).

Main results

• the instance (twoChartModel hF hx).IsSeparated: the two-chart model is a separated scheme; in particular its structure morphism to Spec k is separated.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section II.4 (separated morphisms) and Exercise II.2.12 (gluing).
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Appendix B.

instance TauCeti.AlgebraicGeometry.twoChartModel.instIsSeparated {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : (twoChartModel hF hx).IsSeparated

The two-chart model of a function field is separated. By Mathlib's instances, every morphism out of it, in particular its structure morphism to Spec k, is then separated.