Finite polynomial charts of the two-chart model

For a transcendental function x on an algebraic function field F/k, the finite chart 𝒪_x is the normalization of k[x] in F. Evaluation at x gives the concrete map k[X] → 𝒪_x; it is finite without a separability assumption. The same construction at x⁻¹ gives the chart at infinity. These are the affine maps that glue to the finite map from the two-chart model to the projective line.

Main results

• twoChartModel.polynomialChartMap: evaluation k[X] → 𝒪_x.
• twoChartModel.polynomialChartMap_injective: the map identifies k[X] with k[x].
• twoChartModel.polynomialChartMap_finite: the chart map is finite.
• twoChartModel.isFinite_specMap_polynomialChartMap: the induced morphism of affine schemes is finite.

The finiteness input is TauCeti.IsIntegralClosure.finite_adjoin, transported across Polynomial.algEquivOfTranscendental.

The two affine normalizations are the charts of the projective model in Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.2 and Appendix B.

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.polynomialChartMap {k F : Type u} [Field k] [Field F] [Algebra k F] (x : F) : Polynomial k →ₐ[k] ↥(holomorphyRing {P : Place k F | x ∈ P.integers})

Evaluation at x, regarded as a map from the polynomial chart of the projective line to the corresponding normalization chart of the function field.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.polynomialChartMap_X {k F : Type u} [Field k] [Field F] [Algebra k F] (x : F) : (polynomialChartMap x) Polynomial.X = ⟨x, ⋯⟩

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.polynomialChartMap_C {k F : Type u} [Field k] [Field F] [Algebra k F] (x : F) (c : k) : (polynomialChartMap x) (Polynomial.C c) = (algebraMap k ↥(holomorphyRing {P : Place k F | x ∈ P.integers})) c

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.coe_polynomialChartMap {k F : Type u} [Field k] [Field F] [Algebra k F] (x : F) (p : Polynomial k) : ↑((polynomialChartMap x) p) = (Polynomial.aeval x) p

theorem TauCeti.AlgebraicGeometry.twoChartModel.polynomialChartMap_injective {k F : Type u} [Field k] [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) : Function.Injective ⇑(polynomialChartMap x)

Evaluation into the normalization chart is injective when x is transcendental.

theorem TauCeti.AlgebraicGeometry.twoChartModel.polynomialChartMap_finite {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) : (polynomialChartMap x).Finite

The normalization chart is a finite module over the polynomial chart, including for inseparable extensions of k(X).

theorem TauCeti.AlgebraicGeometry.twoChartModel.isFinite_specMap_polynomialChartMap {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) : AlgebraicGeometry.IsFinite (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (polynomialChartMap x).toRingHom))

The morphism from the normalization chart to the affine chart of ℙ¹_k is finite.