Kummer's theorem: places over a place, from a factorization modulo that place

Let P be a place of an algebraic function field F / k, let F' / k' be a finite extension of F / k, and let y : F' be integral over the valuation ring 𝒪_P, say φ (y) = 0 for a monic φ ∈ 𝒪_P[X] whose image in F[X] is the minimal polynomial of y. Reducing φ modulo the maximal ideal of 𝒪_P gives a polynomial over the residue field F_P, and each monic irreducible factor γ of that reduction produces a place P' of F' / k' over P at which γ (y) vanishes and whose relative degree is at least deg γ; distinct factors produce distinct places. This is the unconditional half of Kummer's theorem, Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 3.3.7.

The construction is direct. A monic lift g ∈ 𝒪_P[X] of γ spans, together with the maximal ideal of 𝒪_P, an ideal of 𝒪_P[y] whose quotient is F_P[X] / (γ), a field; the ideal is therefore proper, and it is nonzero because it contains a uniformizer of P. Stichtenoth's existence theorem for places dominates it by a place P' of F'. The valuation ring of P' then contains 𝒪_P, so P' lies over P; and g (y) lies in the maximal ideal of P', so the residue of y is a root of γ in F'_{P'}. Since γ is irreducible it is the minimal polynomial of that residue over F_P, which both bounds the relative degree below by deg γ and shows that γ is recovered from P' — whence the distinctness of the places attached to distinct factors.

⚠ Kummer's theorem in this unconditional form bounds the splitting of P in F' but does not determine it: the ramification indices are not computed and there may be places over P that no factor of the reduction produces. The complementary statement, that the places produced are all of them with e (P' ∣ P) = ε the multiplicity of γ in the reduction and f (P' ∣ P) = deg γ, needs the monogenicity hypothesis 𝒪'_P = 𝒪_P[y] (Stichtenoth, Corollary 3.3.8) and is not proved here.

Main definitions

• TauCeti.Place.integersEval: evaluation at y : F' of a polynomial over the valuation ring 𝒪_P of a place P of F / k.

Main results

• TauCeti.Place.exists_monic_map_residue_eq: monic polynomials over the residue field F_P lift to monic polynomials over 𝒪_P.
• TauCeti.Place.exists_restrict_eq_of_irreducible_map_residue: Kummer's theorem for a single irreducible factor (Stichtenoth, Theorem 3.3.7).
• TauCeti.Place.map_residue_eq_of_valuation_lt_one: a place over P sees at most one irreducible factor, which is what makes the places of distinct factors distinct.
• TauCeti.Place.exists_injective_restrict_eq: Kummer's theorem, packaged: an injective family of places over P, indexed by a family of monic irreducible factors of the reduction of φ, whose relative degrees are at least the degrees of the factors.

References

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

Evaluating a polynomial integral at a place

noncomputable def TauCeti.Place.integersEval {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) (y : F') : Polynomial ↥P.integers →+* F'

Evaluation at y : F' of a polynomial whose coefficients are integral at the place P of F / k, along the inclusions 𝒪_P ⊆ F ⊆ F'.

Equations

• P.integersEval y = Polynomial.eval₂RingHom ((algebraMap F F').comp (algebraMap (↥P.integers) F)) y

theorem TauCeti.Place.integersEval_eq_aeval_map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] {P : Place k F} (y : F') (g : Polynomial ↥P.integers) : (P.integersEval y) g = (Polynomial.aeval y) (Polynomial.map (algebraMap (↥P.integers) F) g)

@[simp]

theorem TauCeti.Place.integersEval_C {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] {P : Place k F} (y : F') (a : ↥P.integers) : (P.integersEval y) (Polynomial.C a) = (algebraMap F F') ↑a

@[simp]

theorem TauCeti.Place.integersEval_X {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] {P : Place k F} (y : F') : (P.integersEval y) Polynomial.X = y

theorem TauCeti.Place.integersEval_algebraMap {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] {P : Place k F} (y : F') (c : k) : (P.integersEval y) (Polynomial.C ((algebraMap k ↥P.integers) c)) = (algebraMap k F') c

theorem TauCeti.Place.dvd_of_integersEval_eq_zero {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] {P : Place k F} {y : F'} {φ : Polynomial ↥P.integers} (hφ : φ.Monic) (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y) {q : Polynomial ↥P.integers} (hq : (P.integersEval y) q = 0) : φ ∣ q

A polynomial over 𝒪_P vanishing at y is divisible by any monic φ over 𝒪_P whose image in F[X] is the minimal polynomial of y: division by a monic polynomial does not leave 𝒪_P[X], so divisibility may be tested over F.

Integrality of y at a place over P

The residue of y at a place over P

theorem TauCeti.Place.map_residue_eq_of_valuation_lt_one {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'] [FiniteDimensional F F'] {P : Place k F} {P' : Place k' F'} (hres : restrict k F P' = P) {y : F'} (hy : y ∈ P'.integers) {g₁ g₂ : Polynomial ↥P.integers} (hg₁ : g₁.Monic) (hirr₁ : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g₁)) (hv₁ : P'.valuation ((P.integersEval y) g₁) < 1) (hg₂ : g₂.Monic) (hirr₂ : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g₂)) (hv₂ : P'.valuation ((P.integersEval y) g₂) < 1) : Polynomial.map (IsLocalRing.residue ↥P.integers) g₁ = Polynomial.map (IsLocalRing.residue ↥P.integers) g₂

Kummer's theorem sees one factor per place: a place P' over P at which two monic polynomials with irreducible reductions both vanish reduces them to the same irreducible polynomial, namely the minimal polynomial of the residue of y. This is what makes the places attached to distinct irreducible factors of the reduction of φ distinct (Stichtenoth, Theorem 3.3.7).

theorem TauCeti.Place.natDegree_map_residue_le_relativeDegree {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'] [FiniteDimensional F F'] {P : Place k F} {P' : Place k' F'} (hres : restrict k F P' = P) {y : F'} (hy : y ∈ P'.integers) {g : Polynomial ↥P.integers} (hg : g.Monic) (hirr : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g)) (hv : P'.valuation ((P.integersEval y) g) < 1) : (Polynomial.map (IsLocalRing.residue ↥P.integers) g).natDegree ≤ relativeDegree k F P'

The relative degree bound of Kummer's theorem (Stichtenoth, Theorem 3.3.7): a place P' over P at which a monic g with irreducible reduction γ vanishes has relative degree at least deg γ, because γ is the minimal polynomial of the residue of y at P'.

Kummer's theorem

theorem TauCeti.Place.exists_monic_map_residue_eq {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) {γ : Polynomial P.ResidueField} (hγ : γ.Monic) : ∃ (g : Polynomial ↥P.integers), g.Monic ∧ Polynomial.map (IsLocalRing.residue ↥P.integers) g = γ

Every monic polynomial over the residue field F_P lifts to a monic polynomial over the valuation ring 𝒪_P.

theorem TauCeti.Place.exists_restrict_eq_of_irreducible_map_residue {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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (P : Place k F) (y : F') {φ g : Polynomial ↥P.integers} (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y) (hg : g.Monic) (hirr : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g)) (hdvd : Polynomial.map (IsLocalRing.residue ↥P.integers) g ∣ Polynomial.map (IsLocalRing.residue ↥P.integers) φ) : ∃ (P' : Place k' F'), restrict k F P' = P ∧ P'.valuation ((P.integersEval y) g) < 1 ∧ (Polynomial.map (IsLocalRing.residue ↥P.integers) g).natDegree ≤ relativeDegree k F P'

Kummer's theorem (Stichtenoth, Theorem 3.3.7), for one irreducible factor. Let P be a place of F / k, let y : F' be a root of a monic φ ∈ 𝒪_P[X] whose image in F[X] is the minimal polynomial of y, and let g ∈ 𝒪_P[X] be monic with irreducible reduction dividing the reduction of φ. Then some place P' of F' / k' lies over P, has g (y) in its maximal ideal, and has relative degree at least the degree of the reduction of g.

The theorem bounds the splitting of P without determining it: nothing here says that every place over P arises this way, and the ramification indices are not computed.

theorem TauCeti.Place.exists_injective_restrict_eq {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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (P : Place k F) (y : F') {φ : Polynomial ↥P.integers} (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y) {ι : Type u_1} {γ : ι → Polynomial P.ResidueField} (hmonic : ∀ (i : ι), (γ i).Monic) (hirr : ∀ (i : ι), Irreducible (γ i)) (hdvd : ∀ (i : ι), γ i ∣ Polynomial.map (IsLocalRing.residue ↥P.integers) φ) (hinj : Function.Injective γ) : ∃ (Q : ι → Place k' F'), Function.Injective Q ∧ ∀ (i : ι), restrict k F (Q i) = P ∧ (γ i).natDegree ≤ relativeDegree k F (Q i)

Kummer's theorem (Stichtenoth, Theorem 3.3.7), packaged. Let P be a place of F / k and let y : F' be a root of a monic φ ∈ 𝒪_P[X] whose image in F[X] is the minimal polynomial of y. To a family of pairwise distinct monic irreducible factors γ i of the reduction of φ modulo P there is an injective family of places of F' / k' over P, the place attached to γ i having relative degree at least deg (γ i).

The factorization of the reduction of φ therefore bounds the splitting of P in F' / F from below; determining it needs the monogenicity hypothesis of Stichtenoth's Corollary 3.3.8.