The localization of a holomorphy ring away from a function

Let F / k be an algebraic function field, S a set of places of F / k and 𝒪_S its holomorphy ring. For a nonzero x ∈ 𝒪_S, inverting x gives the localization 𝒪_S[1/x], realized inside F by Mathlib's Localization.subalgebra.ofField. This file identifies it: 𝒪_S[1/x] is the holomorphy ring of the places of S at which x⁻¹ is regular. A function regular at those places has its poles on S only among the finitely many zeros of x, so a sufficiently high power of x clears them (TauCeti.exists_pow_mul_mem_holomorphyRing).

The identification is stated for a subalgebra A of F that is, as a set, the holomorphy ring of S, so that it applies to the affine models of F / k as well as to 𝒪_S itself. When A is a Dedekind domain, the places of the localization's finite chart are its height one primes.

Main results

• TauCeti.coe_ofField_powers_eq_holomorphyRing: if a subalgebra A of F is the holomorphy ring of a set S of places and x ∈ A, then the localization A[1/x] ⊆ F is the holomorphy ring of the places of S at which x⁻¹ is regular; TauCeti.mem_ofField_powers_iff_forall_mem_integers is the membership form.
• TauCeti.forall_algebraMap_mem_integers_ofField_powers_iff: the finite chart of A[1/x] is the set of places of S at which x⁻¹ is regular.
• TauCeti.ofFieldPowersHeightOneSpectrumEquiv: for a Dedekind A, the places of that chart are the height one primes of A[1/x].

References

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

theorem TauCeti.coe_ofField_powers_eq_holomorphyRing {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {R : Type u_1} [CommRing R] [Algebra R F] {A : Subalgebra R F} [IsFractionRing (↥A) F] {S : Set (Place k F)} (hF : IsFunctionField k F) (hA : ↑A = ↑(holomorphyRing S)) (x : ↥A) (hx : Submonoid.powers x ≤ nonZeroDivisors ↥A) : ↑(Localization.subalgebra.ofField F (Submonoid.powers x) hx) = ↑(holomorphyRing (S ∩ {P : Place k F | (↑x)⁻¹ ∈ P.integers}))

𝒪_S[1/x] is the holomorphy ring of the places of S at which x⁻¹ is regular. Stated for a subalgebra A of F that is, as a set, the holomorphy ring of S, so that it applies to the affine model R_x as well as to 𝒪_S itself.

theorem TauCeti.mem_ofField_powers_iff_forall_mem_integers {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {R : Type u_1} [CommRing R] [Algebra R F] {A : Subalgebra R F} [IsFractionRing (↥A) F] {S : Set (Place k F)} (hF : IsFunctionField k F) (hA : ↑A = ↑(holomorphyRing S)) (x : ↥A) (hx : Submonoid.powers x ≤ nonZeroDivisors ↥A) {z : F} : z ∈ Localization.subalgebra.ofField F (Submonoid.powers x) hx ↔ ∀ P ∈ S, (↑x)⁻¹ ∈ P.integers → z ∈ P.integers

Membership in 𝒪_S[1/x]: a function lies in the localization exactly when it is regular at every place of S at which x⁻¹ is regular.

theorem TauCeti.forall_algebraMap_mem_integers_ofField_powers_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {R : Type u_1} [CommRing R] [Algebra R F] {A : Subalgebra R F} [IsFractionRing (↥A) F] {S : Set (Place k F)} (hF : IsFunctionField k F) (hA : ↑A = ↑(holomorphyRing S)) (x : ↥A) (hx : Submonoid.powers x ≤ nonZeroDivisors ↥A) {P : Place k F} : (∀ (a : ↥(Localization.subalgebra.ofField F (Submonoid.powers x) hx)), (algebraMap (↥(Localization.subalgebra.ofField F (Submonoid.powers x) hx)) F) a ∈ P.integers) ↔ P ∈ S ∩ {P : Place k F | (↑x)⁻¹ ∈ P.integers}

The finite chart of 𝒪_S[1/x]: a place is finite on the localization exactly when it belongs to S and x⁻¹ is regular there.

noncomputable def TauCeti.ofFieldPowersHeightOneSpectrumEquiv {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {R : Type u_1} [CommRing R] [Algebra R F] {A : Subalgebra R F} [IsFractionRing (↥A) F] {S : Set (Place k F)} [Algebra k ↥A] [IsScalarTower k (↥A) F] [IsDedekindDomain ↥A] (hF : IsFunctionField k F) (hA : ↑A = ↑(holomorphyRing S)) (x : ↥A) (hx : Submonoid.powers x ≤ nonZeroDivisors ↥A) : ↑(S ∩ {P : Place k F | (↑x)⁻¹ ∈ P.integers}) ≃ IsDedekindDomain.HeightOneSpectrum ↥(Localization.subalgebra.ofField F (Submonoid.powers x) hx)

The height one primes of 𝒪_S[1/x] are the places of S at which x⁻¹ is regular, for a Dedekind 𝒪_S: TauCeti.Place.heightOneSpectrumEquiv for the localization, read along the identification of its finite chart.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ofFieldPowersHeightOneSpectrumEquiv_apply {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {R : Type u_1} [CommRing R] [Algebra R F] {A : Subalgebra R F} [IsFractionRing (↥A) F] {S : Set (Place k F)} [Algebra k ↥A] [IsScalarTower k (↥A) F] [IsDedekindDomain ↥A] (hF : IsFunctionField k F) (hA : ↑A = ↑(holomorphyRing S)) (x : ↥A) (hx : Submonoid.powers x ≤ nonZeroDivisors ↥A) (P : ↑(S ∩ {P : Place k F | (↑x)⁻¹ ∈ P.integers})) : (ofFieldPowersHeightOneSpectrumEquiv hF hA x hx) P = (↑P).center ⋯

@[simp]

theorem TauCeti.coe_ofFieldPowersHeightOneSpectrumEquiv_symm_apply {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {R : Type u_1} [CommRing R] [Algebra R F] {A : Subalgebra R F} [IsFractionRing (↥A) F] {S : Set (Place k F)} [Algebra k ↥A] [IsScalarTower k (↥A) F] [IsDedekindDomain ↥A] (hF : IsFunctionField k F) (hA : ↑A = ↑(holomorphyRing S)) (x : ↥A) (hx : Submonoid.powers x ≤ nonZeroDivisors ↥A) (𝔭 : IsDedekindDomain.HeightOneSpectrum ↥(Localization.subalgebra.ofField F (Submonoid.powers x) hx)) : ↑((ofFieldPowersHeightOneSpectrumEquiv hF hA x hx).symm 𝔭) = Place.ofPrime k F 𝔭