The scheme of a function field glued from two affine charts

Let F / k be an algebraic function field and x ∈ F nonzero. The places of F / k at which x is regular and those at which x⁻¹ is regular cover all places. Their holomorphy rings are

• 𝒪_x = holomorphyRing {P | x ∈ 𝒪_P}, the integral closure of k[x] in F, and
• 𝒪_{x⁻¹} = holomorphyRing {P | x⁻¹ ∈ 𝒪_P}, the integral closure of k[x⁻¹] in F

(for the integral closures, see TauCeti.restrictScalars_integralClosure_adjoin_eq_holomorphyRing). Both restrict to the holomorphy ring 𝒪_{x, x⁻¹} of the places at which x is a unit, which is the localization of 𝒪_x away from x and of 𝒪_{x⁻¹} away from x⁻¹ (TauCeti.isLocalization_away_holomorphyRing_inter). Hence Spec 𝒪_{x, x⁻¹} is an open subscheme of both Spec 𝒪_x and Spec 𝒪_{x⁻¹}, and gluing the two charts along it, as the pushout of these two open immersions, gives the integral scheme TauCeti.AlgebraicGeometry.twoChartModel; this is defined for every nonzero x.

When x is transcendental over k, Spec 𝒪_x and Spec 𝒪_{x⁻¹} are the two affine charts of a curve with function field F. For F = k(x) they are Spec k[x] and Spec k[x⁻¹], glued into the projective line; in general they are the normalizations in F of the two standard affine charts of the projective line, and this is the gluing from which the normalization of the projective line in F is built. (When x is algebraic over k, x and x⁻¹ are regular at every place, and the construction does not have this interpretation.)

This file proves that the glued scheme is a quasi-compact integral scheme over k, covered by the two charts, and that for transcendental x its function field is F as a k-algebra.

Main definitions

• TauCeti.AlgebraicGeometry.twoChartModel: the scheme glued from Spec 𝒪_x and Spec 𝒪_{x⁻¹} along Spec 𝒪_{x, x⁻¹}.
• TauCeti.AlgebraicGeometry.twoChartModel.ιFinite and TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity: the open immersions of the two charts.
• TauCeti.AlgebraicGeometry.twoChartModel.chartCover: the open cover by these two charts.
• the instance (twoChartModel hF hx).Over (Spec k), given on each chart by the inclusion of the constants.
• TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv: for x transcendental over k, the k-algebra isomorphism k(X) ≃ₐ[k] F.

Main results

• TauCeti.AlgebraicGeometry.isOpenImmersion_specMap_inclusion_holomorphyRing: Spec of the restriction from the holomorphy ring of S to that of S ∩ {P | x⁻¹ ∈ 𝒪_P} is an open immersion.
• TauCeti.AlgebraicGeometry.twoChartModel.isPushout: the two charts glue along their overlap.
• TauCeti.AlgebraicGeometry.twoChartModel.range_ιFinite_union_range_ιInfinity: the two charts cover the scheme.
• TauCeti.AlgebraicGeometry.twoChartModel.isPullback: the two charts meet exactly in their overlap.
• the instance IsIntegral (twoChartModel hF hx): the scheme is integral.
• the instance CompactSpace (twoChartModel hF hx): the scheme is quasi-compact.
• TauCeti.AlgebraicGeometry.twoChartModel.fromSpec_isAffineOpen_image_ιFinite_top: the canonical morphism from the spectrum of the sections of the finite chart factors through the chart.
• TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_germToFunctionField: the isomorphism k(X) ≃ F sends the germ of a function on the finite chart to that function.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.2 and Appendix B.
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Section I.6 and Exercise II.2.12.

theorem TauCeti.AlgebraicGeometry.isOpenImmersion_specMap_inclusion_holomorphyRing {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {S T : Set (Place k F)} (x : ↥(holomorphyRing S)) (hx : ↑x ≠ 0) (hT : T = S ∩ {P : Place k F | (↑x)⁻¹ ∈ P.integers}) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Subalgebra.inclusion ⋯).toRingHom))

Spec of an inclusion of holomorphy rings that inverts a single function is an open immersion: if T = S ∩ {P | x⁻¹ ∈ 𝒪_P} for a nonzero x ∈ 𝒪_S, then Spec 𝒪_T → Spec 𝒪_S is an open immersion, the scheme-level form of TauCeti.isLocalization_away_holomorphyRing_inter.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.twoChartModel.finiteChartRestriction {k F : Type u} [Field k] [Field F] [Algebra k F] (x : F) : ↥(holomorphyRing {P : Place k F | x ∈ P.integers}) →ₐ[k] ↥(holomorphyRing ({P : Place k F | x ∈ P.integers} ∩ {P : Place k F | x⁻¹ ∈ P.integers}))

The restriction of a function regular wherever x is to the places at which x is a unit.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.twoChartModel.infinityChartRestriction {k F : Type u} [Field k] [Field F] [Algebra k F] (x : F) : ↥(holomorphyRing {P : Place k F | x⁻¹ ∈ P.integers}) →ₐ[k] ↥(holomorphyRing ({P : Place k F | x ∈ P.integers} ∩ {P : Place k F | x⁻¹ ∈ P.integers}))

The restriction of a function regular wherever x⁻¹ is to the places at which x is a unit.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isOpenImmersion_specMap_finiteChartRestriction {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartRestriction x).toRingHom))

Spec 𝒪_{x, x⁻¹} → Spec 𝒪_x is an open immersion: the restriction to the overlap is the localization away from x.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isOpenImmersion_specMap_infinityChartRestriction {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartRestriction x).toRingHom))

Spec 𝒪_{x, x⁻¹} → Spec 𝒪_{x⁻¹} is an open immersion: the restriction to the overlap is the localization away from x⁻¹.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.Scheme

The scheme of F glued from the two charts of x: the pushout of the open immersions Spec 𝒪_x ← Spec 𝒪_{x, x⁻¹} → Spec 𝒪_{x⁻¹}, where 𝒪_x, 𝒪_{x⁻¹} and 𝒪_{x, x⁻¹} are the holomorphy rings of the places at which x, x⁻¹, and both are regular.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.ιFinite {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.Spec ↧↥(holomorphyRing {P : Place k F | x ∈ P.integers}) ⟶ twoChartModel hF hx

The finite chart Spec 𝒪_x of twoChartModel, on which x is regular.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.Spec ↧↥(holomorphyRing {P : Place k F | x⁻¹ ∈ P.integers}) ⟶ twoChartModel hF hx

The chart at infinity Spec 𝒪_{x⁻¹} of twoChartModel, on which x⁻¹ is regular.

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

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

theorem TauCeti.AlgebraicGeometry.twoChartModel.isPushout {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : CategoryTheory.IsPushout (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartRestriction x).toRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartRestriction x).toRingHom)) (ιFinite hF hx) (ιInfinity hF hx)

The two charts glue along their overlap: twoChartModel is the pushout of Spec 𝒪_x ← Spec 𝒪_{x, x⁻¹} → Spec 𝒪_{x⁻¹} along the two chart inclusions.

@[implicit_reducible]

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.chartCover {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : (twoChartModel hF hx).OpenCover

The open cover by the finite chart at false and the chart at infinity at true.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.chartCover_f_false {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : (chartCover hF hx).f false = ιFinite hF hx

The first member of the chart cover is the finite chart inclusion.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.chartCover_f_true {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : (chartCover hF hx).f true = ιInfinity hF hx

The second member of the chart cover is the chart inclusion at infinity.

theorem TauCeti.AlgebraicGeometry.twoChartModel.condition {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartRestriction x).toRingHom)) (ιFinite hF hx) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartRestriction x).toRingHom)) (ιInfinity hF hx)

The two charts agree on their overlap.

theorem TauCeti.AlgebraicGeometry.twoChartModel.condition_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) {Z : AlgebraicGeometry.Scheme} (h : twoChartModel hF hx ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartRestriction x).toRingHom)) (CategoryTheory.CategoryStruct.comp (ιFinite hF hx) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartRestriction x).toRingHom)) (CategoryTheory.CategoryStruct.comp (ιInfinity hF hx) h)

The two charts agree on their overlap.

theorem TauCeti.AlgebraicGeometry.twoChartModel.range_ιFinite_union_range_ιInfinity {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : Set.range ⇑(ιFinite hF hx) ∪ Set.range ⇑(ιInfinity hF hx) = Set.univ

The two charts cover twoChartModel.

theorem TauCeti.AlgebraicGeometry.twoChartModel.range_ιInfinity_inter_range_ιFinite_nonempty {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : (Set.range ⇑(ιInfinity hF hx) ∩ Set.range ⇑(ιFinite hF hx)).Nonempty

The two charts meet. The overlap Spec 𝒪_{x, x⁻¹} is nonempty, and its image lies in both charts.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isPullback {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartRestriction x).toRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartRestriction x).toRingHom)) (ιFinite hF hx) (ιInfinity hF hx)

The two charts meet exactly in their overlap: the square of the gluing is also a pullback, so Spec 𝒪_{x, x⁻¹} is the intersection of Spec 𝒪_x and Spec 𝒪_{x⁻¹} in twoChartModel.

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

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

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

twoChartModel is an integral scheme.

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

twoChartModel is quasi-compact, as the union of its two affine charts.

The structure morphism to Spec k

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.twoChartModel.instOverSpecOf {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : (twoChartModel hF hx).Over (AlgebraicGeometry.Spec ↧k)

The structure morphism of twoChartModel to Spec k, given on each chart by the inclusion of the constants.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_over {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : CategoryTheory.CategoryStruct.comp (ιFinite hF hx) (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k ↥(holomorphyRing {P : Place k F | x ∈ P.integers})))

On the finite chart, the structure morphism is Spec of the inclusion of the constants.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_over_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιFinite hF hx) (CategoryTheory.CategoryStruct.comp (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k ↥(holomorphyRing {P : Place k F | x ∈ P.integers})))) h

On the finite chart, the structure morphism is Spec of the inclusion of the constants.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_over {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : CategoryTheory.CategoryStruct.comp (ιInfinity hF hx) (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k ↥(holomorphyRing {P : Place k F | x⁻¹ ∈ P.integers})))

On the chart at infinity, the structure morphism is Spec of the inclusion of the constants.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_over_assoc {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧k ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιInfinity hF hx) (CategoryTheory.CategoryStruct.comp (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k ↥(holomorphyRing {P : Place k F | x⁻¹ ∈ P.integers})))) h

On the chart at infinity, the structure morphism is Spec of the inclusion of the constants.

The function field

instance TauCeti.AlgebraicGeometry.twoChartModel.instNonemptyCarrierCarrierCommRingCatToSchemeObjOpensSpecOfSubtypeMemSubalgebraHolomorphyRingOfPredPlaceValuationSubringIntegersOpensFunctorιFiniteTop {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : Nonempty ↥↑((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤)

theorem TauCeti.AlgebraicGeometry.twoChartModel.isAffineOpen_image_ιFinite_top {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤)

The finite chart is an affine open subscheme.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.finiteChartSectionsEquiv {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : ↑((twoChartModel hF hx).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤))) ≃+* ↥(holomorphyRing {P : Place k F | x ∈ P.integers})

The functions on the finite chart are the functions of F regular wherever x is.

theorem TauCeti.AlgebraicGeometry.twoChartModel.finiteChartSectionsEquiv_apply {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) (a : ↑((twoChartModel hF hx).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤)))) : (finiteChartSectionsEquiv hF hx) a = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧↥(holomorphyRing {P : Place k F | x ∈ P.integers})).hom) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso (ιFinite hF hx) ⊤).hom) a)

TauCeti.AlgebraicGeometry.twoChartModel.finiteChartSectionsEquiv restricts a function on the finite chart along the chart and reads it as an element of 𝒪_x.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.finiteChartSectionsEquiv_appLE {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) (a : ↑((AlgebraicGeometry.Spec ↧k).presheaf.obj (Opposite.op ⊤))) : (finiteChartSectionsEquiv hF hx) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (twoChartModel hF hx ↘ AlgebraicGeometry.Spec ↧k) ⊤ ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤) ⋯)) a) = (algebraMap k ↥(holomorphyRing {P : Place k F | x ∈ P.integers})) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧k).hom) a)

On the finite chart, the functions on Spec k pulled back along the structure morphism are the constants of 𝒪_x.

theorem TauCeti.AlgebraicGeometry.twoChartModel.fromSpec_isAffineOpen_image_ιFinite_top {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) : ⋯.fromSpec = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartSectionsEquiv hF hx).symm.toRingHom)) (ιFinite hF hx)

The canonical morphism from the spectrum of the sections of the finite chart is Spec of the identification of these sections with 𝒪_x, followed by the chart inclusion.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) : ↑(twoChartModel hF hx).functionField ≃ₐ[k] F

The function field of twoChartModel is F, as a k-algebra, for x transcendental over k. It identifies the germ of a function on the finite chart with that function of F (TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_germToFunctionField).

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_germToFunctionField {k F : Type u} [Field k] [Field F] [Algebra k F] {hF : IsFunctionField k F} {x : F} {hx : x ≠ 0} (hxt : Transcendental k x) (a : ↑((twoChartModel hF hx).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤)))) : (functionFieldEquiv hxt) ((CategoryTheory.ConcreteCategory.hom ((twoChartModel hF hx).germToFunctionField ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤))) a) = ↑((finiteChartSectionsEquiv hF hx) a)

TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv sends the germ of a function on the finite chart to the corresponding function of F.