Holomorphy rings of an algebraic function field

A set S of places of an algebraic function field F / k cuts out the ring

𝒪_S = ⋂_{P ∈ S} 𝒪_P

of functions regular at every place of S — its holomorphy ring. Two extreme cases are already known: 𝒪_∅ = F, and 𝒪_{ℙ_F} is the constant field algebraicClosure k F, which is Stichtenoth's Corollary 1.1.20. This file constructs 𝒪_S in general and proves the two theorems that make the construction a dictionary: 𝒪_S is integrally closed in F, and every k-subalgebra of F integrally closed in F arises this way, from the set of places at which its functions are regular. The two constructions are mutually inverse, since S is recovered from 𝒪_S as the set of places at which every function of 𝒪_S is regular.

Whenever some place lies outside S, the field F is the field of fractions of 𝒪_S, so a holomorphy ring of a proper set of places is a k-subalgebra of F with the same function field — the shape the affine models of TauCeti/FieldTheory/FunctionField/AffineModel/ are built on.

When S is finite, 𝒪_S is moreover a principal ideal domain, and so a Dedekind domain: a nonzero ideal is generated by any of its functions of least order at every place of S at once, and weak approximation manufactures such a function out of the functions of least order at the separate places. A finite S that omits some place is therefore the finite chart of the affine model 𝒪_S, whose height one primes are exactly the places of S; that identification is TauCeti.holomorphyRingHeightOneSpectrumEquiv, in TauCeti/FieldTheory/FunctionField/AffineModel/Prime.lean with the rest of the affine-model dictionary.

The mathematics is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Section III.2. None of it needs an exactness hypothesis on the constant field.

Main definitions

• TauCeti.holomorphyRing: the holomorphy ring 𝒪_S of a set of places, as a k-subalgebra of F.

Main results

• TauCeti.isIntegrallyClosedIn_holomorphyRing: a holomorphy ring is integrally closed in F.
• TauCeti.holomorphyRing_setOf_subset_integers: Stichtenoth, Theorem 3.2.6 — a k-subalgebra of F integrally closed in F is the holomorphy ring of the set of places at which its functions are regular.
• TauCeti.restrictScalars_integralClosure_eq_holomorphyRing: the same theorem for an arbitrary k-subalgebra R of F — the integral closure of R in F is the holomorphy ring of the set of places at which the functions of R are regular.
• TauCeti.coe_holomorphyRing_subset_integers_iff: Stichtenoth, Corollary 3.2.8 — the functions of 𝒪_S are all regular at P exactly when P ∈ S, so S is recovered from 𝒪_S and the two constructions are mutually inverse.
• TauCeti.isFractionRing_holomorphyRing: F is the field of fractions of 𝒪_S as soon as some place lies outside S.
• TauCeti.exists_pow_mul_mem_holomorphyRing: a function regular at every place of S at which x⁻¹ is regular, for some x ∈ 𝒪_S, is made regular on all of S by a power of x.
• TauCeti.dvd_holomorphyRing_iff_forall_ord_le: divisibility in 𝒪_S is the pointwise comparison of orders along S.
• TauCeti.isPrincipalIdealRing_holomorphyRing: Stichtenoth, Proposition 3.2.10 — the holomorphy ring of a finite set of places is a principal ideal domain.
• TauCeti.forall_algebraMap_mem_integers_holomorphyRing_iff: a place is finite on 𝒪_S exactly when it belongs to S, in the form the affine-model dictionary consumes.

Implementation notes

𝒪_S is a Subalgebra k F rather than a bare Subring F: the constants are regular at every place (TauCeti.Place.algebraMap_mem_integers), so the k-algebra structure is free, and it is what the affine-model API consumes. Mathlib's Set.integer, the S-integers of the fraction field of a Dedekind domain, is the same shape for the places of a fixed affine model and with the complementary indexing convention (integrality is imposed away from S); it is not general enough here, where the index is the whole place set of F / k and the place at infinity of a model is a citizen like any other.

Theorem 3.2.6 does not repeat Stichtenoth's Zorn argument. Mathlib's Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn (Stacks 090P) already separates an element from a subring integrally closed in a field by a valuation subring; what is specific to function fields is that the valuation subring so produced is a place, and that is TauCeti.Place.ofValuationSubring.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.2 (Definition 3.2.2, Theorem 3.2.6, Corollary 3.2.8, Proposition 3.2.10).

The holomorphy ring of a set of places

def TauCeti.holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (S : Set (Place k F)) : Subalgebra k F

The holomorphy ring 𝒪_S = ⋂_{P ∈ S} 𝒪_P of a set S of places of F / k (Stichtenoth, Definition 3.2.2): the functions regular at every place of S.

Equations

• TauCeti.holomorphyRing S = { carrier := {z : F | ∀ P ∈ S, z ∈ P.integers}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_holomorphyRing_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} {z : F} : z ∈ holomorphyRing S ↔ ∀ P ∈ S, z ∈ P.integers

theorem TauCeti.mem_holomorphyRing_iff_forall_ord_nonneg {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} {z : F} : z ∈ holomorphyRing S ↔ ∀ P ∈ S, 0 ≤ P.ord z

Membership in 𝒪_S in additive form: z has no pole on S.

theorem TauCeti.coe_holomorphyRing_subset_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} {P : Place k F} (hP : P ∈ S) : ↑(holomorphyRing S) ⊆ ↑P.integers

Every function of 𝒪_S is regular at every place of S.

theorem TauCeti.holomorphyRing_antitone {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : Antitone holomorphyRing

Asking for regularity at more places gives a smaller ring.

@[simp]

theorem TauCeti.holomorphyRing_empty {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : holomorphyRing ∅ = ⊤

@[simp]

theorem TauCeti.holomorphyRing_univ {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : holomorphyRing Set.univ = (algebraicClosure k F).toSubalgebra

The holomorphy ring of all the places is the constant field (Stichtenoth, Corollary 1.1.20): a function regular everywhere is algebraic over k.

instance TauCeti.isIntegrallyClosedIn_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (S : Set (Place k F)) : IsIntegrallyClosedIn (↥(holomorphyRing S)) F

A holomorphy ring is integrally closed in F: a function integral over 𝒪_S is integral over each 𝒪_P with P ∈ S, and a valuation ring is integrally closed (TauCeti.Place.mem_integers_of_isIntegral).

The field of fractions

theorem TauCeti.exists_ne_zero_mem_holomorphyRing_and_mul_mem {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {S : Set (Place k F)} {Q : Place k F} (hQ : Q ∉ S) (z : F) : ∃ (y : F), y ≠ 0 ∧ y ∈ holomorphyRing S ∧ y * z ∈ holomorphyRing S

Denominators regular on S: if some place Q lies outside S, every function of F is (y * z) / y for a nonzero y with y and y * z both regular on S. Riemann's theorem supplies y inside L(n·Q - (z)_∞) for n large: such a y vanishes on the poles of z to at least their order, and its own only pole is Q, which lies outside S.

theorem TauCeti.isFractionRing_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {S : Set (Place k F)} (hS : Sᶜ.Nonempty) : IsFractionRing (↥(holomorphyRing S)) F

F is the field of fractions of 𝒪_S whenever some place lies outside S (Stichtenoth, Section III.2).

Clearing poles by a power of a function

theorem TauCeti.exists_pow_mul_mem_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {S : Set (Place k F)} {x : F} (hx : x ∈ holomorphyRing S) {z : F} (hz : ∀ P ∈ S, x⁻¹ ∈ P.integers → z ∈ P.integers) : ∃ (n : ℕ), x ^ n * z ∈ holomorphyRing S

A function regular at every place of S at which x⁻¹ is regular is made regular on all of S by a sufficiently high power of x ∈ 𝒪_S: its poles on S are among the finitely many zeros of x.

Integrally closed subrings are holomorphy rings

theorem TauCeti.holomorphyRing_setOf_subset_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (R : Subalgebra k F) [IsIntegrallyClosedIn (↥R) F] : holomorphyRing {P : Place k F | ↑R ⊆ ↑P.integers} = R

Stichtenoth, Theorem 3.2.6. A k-subalgebra of F that is integrally closed in F is the holomorphy ring of the set of places at which all of its functions are regular. No hypothesis on the constant field is needed.

A function outside R is separated from R by a valuation subring of F (Subring.exists_le_valuationSubring_of_isIntegrallyClosedIn), which contains the constants and is proper, hence is the valuation ring of a place.

theorem TauCeti.restrictScalars_integralClosure_eq_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (R : Subalgebra k F) : Subalgebra.restrictScalars k (integralClosure (↥R) F) = holomorphyRing {P : Place k F | ↑R ⊆ ↑P.integers}

Stichtenoth, Theorem 3.2.6, for an arbitrary k-subalgebra: the integral closure of R in F is the holomorphy ring of the set of places at which all the functions of R are regular.

Recovering the set of places

@[simp]

theorem TauCeti.coe_holomorphyRing_subset_integers_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {S : Set (Place k F)} {P : Place k F} : ↑(holomorphyRing S) ⊆ ↑P.integers ↔ P ∈ S

Stichtenoth, Corollary 3.2.8. The functions of 𝒪_S are all regular at a place P exactly when P belongs to S, so S is recovered from its holomorphy ring: together with TauCeti.holomorphyRing_setOf_subset_integers this makes sets of places and k-subalgebras of F integrally closed in F correspond antitonely.

Finitely many places: a principal ideal domain

theorem TauCeti.ord_nonneg_of_mem_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} {P : Place k F} (hP : P ∈ S) (z : ↥(holomorphyRing S)) : 0 ≤ P.ord ↑z

The functions of 𝒪_S have nonnegative order at every place of S.

theorem TauCeti.dvd_holomorphyRing_iff_forall_ord_le {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} {t z : ↥(holomorphyRing S)} (ht : ↑t ≠ 0) (hz : ↑z ≠ 0) : t ∣ z ↔ ∀ P ∈ S, P.ord ↑t ≤ P.ord ↑z

Divisibility in 𝒪_S is a pointwise comparison of orders: a nonzero function of 𝒪_S divides another exactly when it vanishes to no greater order at every place of S. The hypotheses exclude the junk value ord_P 0 = 0; 0 is of course divisible by everything.

theorem TauCeti.isPrincipalIdealRing_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} (hS : S.Finite) : IsPrincipalIdealRing ↥(holomorphyRing S)

Stichtenoth, Proposition 3.2.10: the holomorphy ring of a finite set S of places of F / k is a principal ideal domain. Only the finiteness of S is used — weak approximation at finitely many distinct places needs no hypothesis on k or on F / k — so this does not ask F / k to be an algebraic function field. A nonzero ideal is generated by any of its functions of least order at every place of S at once, which weak approximation manufactures out of the functions of least order at the separate places, since 𝒪_S is then divided by such a function (TauCeti.dvd_holomorphyRing_iff_forall_ord_le). In particular 𝒪_S is a Dedekind domain, by IsPrincipalIdealRing.isDedekindDomain, and so — with TauCeti.isFractionRing_holomorphyRing — an affine model, whose height one primes are the places of S; that is holomorphyRingHeightOneSpectrumEquiv, downstream in TauCeti/FieldTheory/FunctionField/AffineModel/Prime.lean.

Holomorphy rings as affine models

theorem TauCeti.forall_algebraMap_mem_integers_holomorphyRing_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {S : Set (Place k F)} (hF : IsFunctionField k F) {P : Place k F} : (∀ (r : ↥(holomorphyRing S)), (algebraMap (↥(holomorphyRing S)) F) r ∈ P.integers) ↔ P ∈ S

A place of F / k is finite on 𝒪_S exactly when it belongs to S (TauCeti.coe_holomorphyRing_subset_integers_iff, in the form the affine-model dictionary consumes). It is deliberately not a simp lemma: simp unfolds both TauCeti.holomorphyRing membership and TauCeti.Place.integers membership into valuation inequalities, so this left-hand side is not in simp normal form.