Holomorphy rings in an extension: 𝒪'_P is the integral closure of 𝒪_P

Let F' / k' be an extension of the algebraic function field F / k, integral both on the constants and on the functions. Every place P' of F' / k' restricts to a place P'.restrict k F of F / k (TauCeti.Place.restrict), and at a single place P the integral closure 𝒪'_P of 𝒪_P in F' is already known to be the intersection of the valuation rings of the fibre over P (TauCeti.Place.isIntegral_iff_forall_restrict_eq_mem_integers). This file extends that computation from one place to a set of them: for a set S of places of F / k, the intersection of the valuation rings 𝒪_{P'} over the places P' lying over S is the integral closure of the holomorphy ring 𝒪_S = ⋂_{P ∈ S} 𝒪_P in F'. So integrality over an arbitrary holomorphy ring is regularity above its defining set of places.

It also reads the fibre back off the integral closure: the places of F' / k' at which every function of 𝒪'_P is regular are exactly the places over P, and likewise over a set.

Main results

• TauCeti.coe_holomorphyRing_setOf_restrict_mem and TauCeti.mem_holomorphyRing_setOf_restrict_mem_iff_isIntegral: the holomorphy ring of the places lying over S is the integral closure of 𝒪_S in F', in set and membership form.
• TauCeti.coe_integralClosure_integers_subset_integers_iff: the places of F' / k' at which every function of 𝒪'_P is regular are exactly the places over P, so 𝒪'_P remembers the fibre; TauCeti.coe_integralClosure_holomorphyRing_subset_integers_iff is the version over a set of places.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections III.2 and III.3. The description of the integral closure of 𝒪_P in F' as the intersection of the valuation rings of the places over P is the opening result of Section III.3, on which its local integral bases rest.

The integral closure of a holomorphy ring

theorem TauCeti.mem_holomorphyRing_setOf_restrict_mem_iff_isIntegral {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') {S : Set (Place k F)} {z : F'} : z ∈ holomorphyRing {P' : Place k' F' | Place.restrict k F P' ∈ S} ↔ IsIntegral (↥(holomorphyRing S)) z

The integral closure of a holomorphy ring, over a set of places: a function of F' is regular at every place of F' / k' lying over S exactly when it is integral over the holomorphy ring 𝒪_S (Stichtenoth, Section III.3).

theorem TauCeti.coe_holomorphyRing_setOf_restrict_mem {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (S : Set (Place k F)) : ↑(holomorphyRing {P' : Place k' F' | Place.restrict k F P' ∈ S}) = ↑(integralClosure (↥(holomorphyRing S)) F')

The integral closure of a holomorphy ring, over a set of places: the holomorphy ring of the places of F' / k' lying over S is the integral closure of 𝒪_S in F' (Stichtenoth, Section III.3).

Recovering the fibre from the integral closure

@[simp]

theorem TauCeti.coe_integralClosure_holomorphyRing_subset_integers_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (S : Set (Place k F)) (P' : Place k' F') : ↑(integralClosure (↥(holomorphyRing S)) F') ⊆ ↑P'.integers ↔ Place.restrict k F P' ∈ S

The places of F' / k' at which every function of the integral closure of 𝒪_S is regular are exactly the places lying over S (Stichtenoth, Corollary 3.2.8 read through the theorem above).

@[simp]

theorem TauCeti.coe_integralClosure_integers_subset_integers_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k' F') (P : Place k F) (P' : Place k' F') : ↑(integralClosure (↥P.integers) F') ⊆ ↑P'.integers ↔ Place.restrict k F P' = P

The places of F' / k' at which every function of 𝒪'_P is regular are exactly the places lying over P, so the fibre over P is recovered from 𝒪'_P (Stichtenoth, Corollary 3.2.8 read through TauCeti.Place.isIntegral_iff_forall_restrict_eq_mem_integers). Unlike the version over a set of places, this needs no hypothesis on F / k.