The morphism of two-chart models induced by an extension of function fields

Let F' / F be an integral extension of algebraic function fields over k, let x ∈ F be nonzero, and let x' ∈ F' be its image. A place of F' at which x' is regular lies over a place of F at which x is regular, so F → F' maps the holomorphy ring 𝒪_x of F into the holomorphy ring 𝒪_{x'} of F', and likewise 𝒪_{x⁻¹} into 𝒪_{x'⁻¹} and the overlap ring into the overlap ring. For x transcendental over k, on the finite charts this is the inclusion of the integral closure of k[x] in F into the integral closure of k[x] in F'. Taking spectra, the two chart maps agree on the overlap, so they glue to a morphism of schemes over k

twoChartModel hF' hx' ⟶ twoChartModel hF hx

(TauCeti.AlgebraicGeometry.twoChartModel.map). It is dominant, and for x transcendental over k the pullback of rational functions along it is F → F', read through the identifications of the function fields of the two models with F and F'. The construction is functorial: the identity of F induces the identity, and a tower F → F' → F'' induces the composite.

For x transcendental over k, this is the morphism of normalized models of the projective line attached to an embedding of function fields, the morphism part of the correspondence between function fields and regular projective curves.

Main definitions

• TauCeti.AlgebraicGeometry.twoChartModel.finiteChartMap, TauCeti.AlgebraicGeometry.twoChartModel.infinityChartMap: the maps 𝒪_x → 𝒪_{x'} and 𝒪_{x⁻¹} → 𝒪_{x'⁻¹} of chart rings induced by F → F'.
• TauCeti.AlgebraicGeometry.twoChartModel.map: the morphism of two-chart models induced by F → F'.

Main results

• TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_map and TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_map: on each chart, map is Spec of the chart map.
• the instances (map …).IsOver (Spec k) and IsDominant (map …).
• TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_functionFieldMap_map: the pullback of rational functions along map is F → F'.
• TauCeti.AlgebraicGeometry.twoChartModel.map_id and TauCeti.AlgebraicGeometry.twoChartModel.map_comp: functoriality.

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 (the morphism of abstract nonsingular curves attached to an embedding of function fields).

The chart maps

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.finiteChartMap {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] {x : F} {x' : F'} (h : (algebraMap F F') x = x') : ↥(holomorphyRing {P : Place k F | x ∈ P.integers}) →+* ↥(holomorphyRing {P' : Place k F' | x' ∈ P'.integers})

The map 𝒪_x → 𝒪_{x'} of finite charts induced by F → F', where x' is the image of x: a place of F' at which x' is regular lies over a place of F at which x is regular.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coe_finiteChartMap_apply {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] {x : F} {x' : F'} (h : (algebraMap F F') x = x') (z : ↥(holomorphyRing {P : Place k F | x ∈ P.integers})) : ↑((finiteChartMap h) z) = (algebraMap F F') ↑z

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.infinityChartMap {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] {x : F} {x' : F'} (h : (algebraMap F F') x = x') : ↥(holomorphyRing {P : Place k F | x⁻¹ ∈ P.integers}) →+* ↥(holomorphyRing {P' : Place k F' | x'⁻¹ ∈ P'.integers})

The map 𝒪_{x⁻¹} → 𝒪_{x'⁻¹} of charts at infinity induced by F → F', where x' is the image of x.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coe_infinityChartMap_apply {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] {x : F} {x' : F'} (h : (algebraMap F F') x = x') (z : ↥(holomorphyRing {P : Place k F | x⁻¹ ∈ P.integers})) : ↑((infinityChartMap h) z) = (algebraMap F F') ↑z

The morphism of models

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.map {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') : twoChartModel hF' hx' ⟶ twoChartModel hF hx

The morphism of two-chart models induced by F → F': for x' ∈ F' the image of x ∈ F, the morphism twoChartModel hF' hx' ⟶ twoChartModel hF hx glued from Spec of the chart maps 𝒪_x → 𝒪_{x'} and 𝒪_{x⁻¹} → 𝒪_{x'⁻¹}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_map {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') : CategoryTheory.CategoryStruct.comp (ιFinite hF' hx') (map hF hF' hx hx' h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartMap h))) (ιFinite hF hx)

On the finite chart, map is Spec of the map 𝒪_x → 𝒪_{x'}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιFinite_map_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') {Z : AlgebraicGeometry.Scheme} (h✝ : twoChartModel hF hx ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιFinite hF' hx') (CategoryTheory.CategoryStruct.comp (map hF hF' hx hx' h) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartMap h))) (CategoryTheory.CategoryStruct.comp (ιFinite hF hx) h✝)

On the finite chart, map is Spec of the map 𝒪_x → 𝒪_{x'}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_map {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') : CategoryTheory.CategoryStruct.comp (ιInfinity hF' hx') (map hF hF' hx hx' h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartMap h))) (ιInfinity hF hx)

On the chart at infinity, map is Spec of the map 𝒪_{x⁻¹} → 𝒪_{x'⁻¹}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.ιInfinity_map_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') {Z : AlgebraicGeometry.Scheme} (h✝ : twoChartModel hF hx ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιInfinity hF' hx') (CategoryTheory.CategoryStruct.comp (map hF hF' hx hx' h) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartMap h))) (CategoryTheory.CategoryStruct.comp (ιInfinity hF hx) h✝)

On the chart at infinity, map is Spec of the map 𝒪_{x⁻¹} → 𝒪_{x'⁻¹}.

instance TauCeti.AlgebraicGeometry.twoChartModel.instIsOverMapSpecOf {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') : AlgebraicGeometry.Scheme.Hom.IsOver (map hF hF' hx hx' h) (AlgebraicGeometry.Spec ↧k)

map is a morphism of schemes over k.

instance TauCeti.AlgebraicGeometry.twoChartModel.instIsDominantMap {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') : AlgebraicGeometry.IsDominant (map hF hF' hx hx' h)

map is dominant: the finite chart of twoChartModel hF' hx' is dense, and on it map is Spec of the injective map 𝒪_x → 𝒪_{x'} followed by an open immersion with dense image.

Functions on the finite charts and the function field

theorem TauCeti.AlgebraicGeometry.twoChartModel.image_ιFinite_top_le_preimage_map {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') : (AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF' hx')).obj ⊤ ≤ (TopologicalSpace.Opens.map (map hF hF' hx hx' h).base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤)

map sends the finite chart of twoChartModel hF' hx' into the finite chart of twoChartModel hF hx.

theorem TauCeti.AlgebraicGeometry.twoChartModel.finiteChartSectionsEquiv_map_appLE {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (s : ↑((twoChartModel hF hx).presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤)))) : (finiteChartSectionsEquiv hF' hx') ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE (map hF hF' hx hx' h) ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF hx)).obj ⊤) ((AlgebraicGeometry.Scheme.Hom.opensFunctor (ιFinite hF' hx')).obj ⊤) ⋯)) s) = (finiteChartMap h) ((finiteChartSectionsEquiv hF hx) s)

On the finite charts, map acts on functions as F → F': pulling a function of 𝒪_x back along map and restricting it to the finite chart of twoChartModel hF' hx' gives its image in 𝒪_{x'}.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_functionFieldMap_map {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) (z : F) : (functionFieldEquiv ⋯) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.functionFieldMap (map hF hF' hx hx' h))) ((functionFieldEquiv hxt).symm z)) = (algebraMap F F') z

The pullback of rational functions along map is F → F': for x transcendental over k, under the identifications k(X) ≃ F and k(X') ≃ F' of the function fields of the two models, the pullback along map : X' ⟶ X is the algebra map F → F'.

Functoriality

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.map_id {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) (h : (algebraMap F F) x = x) : map hF hF hx hx h = CategoryTheory.CategoryStruct.id (twoChartModel hF hx)

The identity of F induces the identity of twoChartModel hF hx.

theorem TauCeti.AlgebraicGeometry.twoChartModel.map_comp {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') {F'' : Type u} [Field F''] [Algebra k F''] [Algebra F' F''] [Algebra F F''] [IsScalarTower k F' F''] [IsScalarTower k F F''] [IsScalarTower F F' F''] [Algebra.IsIntegral F' F''] [Algebra.IsIntegral F F''] (hF'' : IsFunctionField k F'') {x'' : F''} (hx'' : x'' ≠ 0) (h' : (algebraMap F' F'') x' = x'') (h'' : (algebraMap F F'') x = x'') : CategoryTheory.CategoryStruct.comp (map hF' hF'' hx' hx'' h') (map hF hF' hx hx' h) = map hF hF'' hx hx'' h''

A tower F → F' → F'' induces the composite of the morphisms of two-chart models.

theorem TauCeti.AlgebraicGeometry.twoChartModel.map_comp_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') {F'' : Type u} [Field F''] [Algebra k F''] [Algebra F' F''] [Algebra F F''] [IsScalarTower k F' F''] [IsScalarTower k F F''] [IsScalarTower F F' F''] [Algebra.IsIntegral F' F''] [Algebra.IsIntegral F F''] (hF'' : IsFunctionField k F'') {x'' : F''} (hx'' : x'' ≠ 0) (h' : (algebraMap F' F'') x' = x'') (h'' : (algebraMap F F'') x = x'') {Z : AlgebraicGeometry.Scheme} (h✝ : twoChartModel hF hx ⟶ Z) : CategoryTheory.CategoryStruct.comp (map hF' hF'' hx' hx'' h') (CategoryTheory.CategoryStruct.comp (map hF hF' hx hx' h) h✝) = CategoryTheory.CategoryStruct.comp (map hF hF'' hx hx'' h'') h✝

A tower F → F' → F'' induces the composite of the morphisms of two-chart models.