The affine model `R_x`: the integral closure of `k[x]` #

Let F / k be an algebraic function field and x ∈ F transcendental over k. The integral closure

R_x = integralClosure k[x] F

of the polynomial ring k[x] = Algebra.adjoin k {x} in F is the standard affine model of F / k attached to x: the coordinate ring of the part of the curve where x has no pole. This file shows that R_x has every property the affine-model API of TauCeti/FieldTheory/FunctionField/AffineModel/ asks of a model, with no separability hypothesis on F / k(x):

R_x is a Dedekind domain with fraction field F;
its functions are exactly those whose poles are among the poles of x, that is, R_x is the holomorphy ring of the places at which x is regular;
hence its finite chart consists of the places at which x has no pole, and those places are in bijection with the height one primes of R_x.

The places missing from the finite chart are the poles of x, of which there are finitely many (TauCeti.Place.finite_setOf_ord_neg).

Main results #

TauCeti.isDedekindDomain_integralClosure_adjoin and TauCeti.isFractionRing_integralClosure_adjoin: R_x is a Dedekind domain with fraction field F.
TauCeti.restrictScalars_integralClosure_adjoin_eq_holomorphyRing and TauCeti.mem_integralClosure_adjoin_iff: a function lies in R_x exactly when it is regular at every place at which x is regular.
TauCeti.Place.forall_algebraMap_mem_integers_integralClosure_adjoin_iff: a place is finite on R_x exactly when x has no pole there.
TauCeti.integralClosureAdjoinHeightOneSpectrumEquiv: the places at which x has no pole are in bijection with the height one primes of R_x.

References #

H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.2.

The finite chart of `R_x` #

source

@[simp]

theorem TauCeti.Place.forall_algebraMap_mem_integers_integralClosure_adjoin_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {x : F} :

(∀ a ∈ integralClosure (↥k[x]) F, P.valuation a ≤ 1) ↔ x ∈ P.integers

The finite chart of R_x: a place P is finite on the integral closure of k[x] in F exactly when x has no pole at P.

`R_x` as a holomorphy ring #

source

theorem TauCeti.restrictScalars_integralClosure_adjoin_eq_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : F) :

Subalgebra.restrictScalars k (integralClosure (↥k[x]) F) = holomorphyRing {P : Place k F | x ∈ P.integers}

R_x is the holomorphy ring of the places at which x is regular (Stichtenoth, Section III.2): the integral closure of k[x] in F consists of the functions of F that are regular wherever x is. This is Stichtenoth's Theorem 3.2.6 for k[x], whose functions are all regular at a place exactly when x is.

source

theorem TauCeti.mem_integralClosure_adjoin_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x z : F} :

z ∈ integralClosure (↥k[x]) F ↔ ∀ (P : Place k F), x ∈ P.integers → z ∈ P.integers

A function is integral over k[x] exactly when its poles are among the poles of x: it lies in R_x exactly when it is regular at every place at which x is regular.

`R_x` is an affine model #

source

theorem TauCeti.isDedekindDomain_integralClosure_adjoin {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hx : Transcendental k x) :

IsDedekindDomain ↥(integralClosure (↥k[x]) F)

R_x is a Dedekind domain: the integral closure of k[x] in an algebraic function field F, for x transcendental over k. No separability of F / k(x) is assumed.

source