Abhyankar's lemma

Let F' / F be a finite separable extension of function fields, F₁ and F₂ intermediate fields, and P' a place of the compositum F₁ F₂ lying over P₁ in F₁, P₂ in F₂ and P in F. If the residue field of P is perfect (for instance if the constant field is perfect) and the ramification index e(P₁ ∣ P) is prime to the characteristic, then

e(P' ∣ P) = lcm (e(P₁ ∣ P), e(P₂ ∣ P)).

This controls ramification in composita, for instance in towers of function fields built by successive composita; in particular a compositum of two extensions in which P has ramification index 1 again has ramification index 1 over P.

The proof is group-theoretic. Embed everything in a finite Galois extension and let I be the inertia group of a place Q above P'. When the residue extension at Q is separable, the ramification index of Q over F is |I|, so the ramification index over F of the restriction of Q to an intermediate field E is the index in I of the elements fixing E (TauCeti.Place.ramificationIdx_restrict_eq_relIndex). The wild inertia group I₁ is a normal p-subgroup of I with I / I₁ cyclic of order prime to p; for such a group, the index of an intersection A ⊓ B is the least common multiple of the indices as soon as [I : A] is prime to p (Subgroup.index_inf_eq_lcm_of_isCyclic_quotient).

Main results

• TauCeti.Place.ramificationIdx_restrict_sup_of_isGalois: Abhyankar's lemma for intermediate fields of a finite Galois extension with separable residue extension.
• TauCeti.Place.ramificationIdx_restrict_sup: Abhyankar's lemma for intermediate fields of a finite separable extension, when the residue field of the place below is perfect (for instance when the constant field is perfect, by TauCeti.Place.perfectField_residueField).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.9.1.
• J.-P. Serre, Local Fields, GTM 67, Springer, 1979, Chapter IV, Corollaries 1–4 of Proposition 7, for the structure of the inertia group.

theorem TauCeti.Place.ramificationIdx_restrict_sup_of_isGalois {k : Type u} {F : Type v} {F' : Type w} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [IsGalois F F'] (Q : Place k F') [Algebra.IsSeparable (restrict k F Q).ResidueField Q.ResidueField] (E₁ E₂ : IntermediateField F F') (h₁ : ↑(ramificationIdx F (restrict k (↥E₁) Q)) ≠ 0) : ramificationIdx F (restrict k (↥(E₁ ⊔ E₂)) Q) = (ramificationIdx F (restrict k (↥E₁) Q)).lcm (ramificationIdx F (restrict k (↥E₂) Q))

Abhyankar's lemma in a Galois extension (Stichtenoth, Theorem 3.9.1). Let E₁ and E₂ be intermediate fields of a finite Galois extension F' / F and Q a place of F' whose residue extension over F is separable. If the ramification index of Q ∩ E₁ over F is nonzero in k, then the ramification index of Q ∩ E₁ E₂ over F is the least common multiple of those of Q ∩ E₁ and Q ∩ E₂.

The hypothesis on E₁ cannot be dropped. Over F = 𝔽_p(x), the Artin–Schreier extensions y₁ ^ p - y₁ = x and y₂ ^ p - y₂ = x ^ (p + 1) are totally ramified of degree p at the pole of x, and so is every other subextension of degree p of their compositum, which is therefore totally ramified of degree p ^ 2 there.

theorem TauCeti.Place.ramificationIdx_restrict_sup {k : Type u} {F : Type v} {F' : Type w} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : IsFunctionField k F) (P' : Place k F') [PerfectField (restrict k F P').ResidueField] (E₁ E₂ : IntermediateField F F') (h₁ : ↑(ramificationIdx F (restrict k (↥E₁) P')) ≠ 0) : ramificationIdx F (restrict k (↥(E₁ ⊔ E₂)) P') = (ramificationIdx F (restrict k (↥E₁) P')).lcm (ramificationIdx F (restrict k (↥E₂) P'))

Abhyankar's lemma (Stichtenoth, Theorem 3.9.1). Let E₁ and E₂ be intermediate fields of a finite separable extension F' / F of function fields, and P' a place of F' such that the residue field of the place P below it in F is perfect, for instance because k is perfect (TauCeti.Place.perfectField_residueField). If the ramification index of P' ∩ E₁ over P is nonzero in k, then the ramification index of P' ∩ E₁ E₂ over P is the least common multiple of those of P' ∩ E₁ and P' ∩ E₂.

In particular, if P' ∩ E₁ and P' ∩ E₂ have ramification index 1 over P, then so does P' ∩ E₁ E₂.