Places in a purely inseparable extension

Let F' / k' be an extension of the field extension F / k in which F' / F is purely inseparable: every z ∈ F' has a power z ^ q ^ n in F, where q is the exponential characteristic. Such an extension is invisible to places in the following sense.

• A place of F has at most one place of F' above it. Whether z is regular at a place P' of F' is decided by whether its power z ^ q ^ n ∈ F is regular at the place P below, so the valuation ring of P' — and hence P' itself — is determined by P. Together with the existence of extensions of places (TauCeti.Place.restrict_surjective), there is exactly one.
• The fundamental identity has a single term: at a place of an algebraic function field F / k and for F' / F finite, e(P' ∣ P) · f(P' ∣ P) = [F' : F].
• The residue extension is purely inseparable, since the residue of z has the residue of z ^ q ^ n as a q ^ n-th power.

In particular, for a purely inseparable step of prime degree p the product e · f is p, so the place is either totally ramified (e = p, f = 1) or has residue degree p (e = 1, f = p). The clean conclusion e = [F' : F], f = 1 holds as soon as the residue extension is also separable — for instance when the residue field of P is perfect, which is automatic over a perfect constant field — because an extension that is both separable and purely inseparable is trivial.

Without that hypothesis the conclusion fails, and the last section proves the standard counterexample. Let k have characteristic p and let s ∈ k not be a p-th power. In F' = k(x) over F = k(t) with t = x ^ p, the place P' of x ^ p − s lies over the zero P of t − s, and e(P' ∣ P) = 1, f(P' ∣ P) = p: the residue field of P is k, while that of P' is k(s^{1/p}).

Main results

• TauCeti.Place.restrict_injective_of_isPurelyInseparable: in a purely inseparable extension, distinct places lie over distinct places; with the existence of extensions this is TauCeti.Place.restrict_bijective_of_isPurelyInseparable, a unique place above each place.
• TauCeti.Place.ramificationIdx_mul_relativeDegree_eq_finrank_of_isPurelyInseparable: e(P' ∣ P) · f(P' ∣ P) = [F' : F] for every place P' of a finite purely inseparable extension of an algebraic function field.
• TauCeti.Place.isPurelyInseparable_residueField: the residue extension at a place of a purely inseparable extension is purely inseparable.
• TauCeti.Place.relativeDegree_eq_one_of_isPurelyInseparable and TauCeti.Place.ramificationIdx_eq_finrank_of_isPurelyInseparable: f(P' ∣ P) = 1 and e(P' ∣ P) = [F' : F] when the residue extension is separable.
• TauCeti.Place.ramificationIdx_adicOfIrreducible_X_pow_sub_C, TauCeti.Place.ord_restrict_adicOfIrreducible_X_pow_sub_C and TauCeti.Place.relativeDegree_adicOfIrreducible_X_pow_sub_C: the counterexample e = 1, f = p in k(x) / k(x ^ p) at the zero of x ^ p − s.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.10, where the base field is assumed perfect throughout.

theorem TauCeti.Place.mem_integers_iff_of_algebraMap_eq_pow (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 F F'] (P' : Place k' F') {z : F'} {m : ℕ} {a : F} (hm : m ≠ 0) (ha : (algebraMap F F') a = z ^ m) : z ∈ P'.integers ↔ a ∈ (restrict k F P').integers

An element z of F' with a positive power z ^ m in F is regular at a place P' of F' / k' exactly when that power is regular at the place of F / k below P'.

theorem TauCeti.Place.restrict_injective_of_isPurelyInseparable (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'] [IsPurelyInseparable F F'] : Function.Injective fun (P' : Place k' F') => restrict k F P'

A place has at most one extension in a purely inseparable extension: two places of F' / k' lying over the same place of F / k are equal. Each element of F' has a power in F, and whether it is regular at a place above P is read off that power at P.

With TauCeti.Place.restrict_surjective, every place of F / k has exactly one extension; that is TauCeti.Place.restrict_bijective_of_isPurelyInseparable.

theorem TauCeti.Place.restrict_bijective_of_isPurelyInseparable (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'] [IsPurelyInseparable F F'] [Algebra.IsIntegral k k'] (hF' : IsFunctionField k' F') : Function.Bijective fun (P' : Place k' F') => restrict k F P'

A place has exactly one extension in a purely inseparable extension: if F' / k' is an algebraic function field and k' / k is integral, restriction is a bijection from the places of F' / k' to the places of F / k.

theorem TauCeti.Place.ramificationIdx_mul_relativeDegree_eq_finrank_of_isPurelyInseparable (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'] [IsPurelyInseparable F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (P' : Place k' F') : ramificationIdx F P' * relativeDegree k F P' = Module.finrank F F'

The fundamental identity in a purely inseparable extension: for a finite purely inseparable extension F' / F of an algebraic function field F / k, the place P' is the only place over the place P below it, so e(P' ∣ P) · f(P' ∣ P) = [F' : F]. No separability of the residue extension is assumed.

instance TauCeti.Place.isPurelyInseparable_residueField {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'] [IsPurelyInseparable F F'] (P' : Place k' F') : IsPurelyInseparable (restrict k F P').ResidueField P'.ResidueField

The residue extension of a purely inseparable extension is purely inseparable: the residue of z ∈ 𝒪_{P'} has the residue of the power z ^ q ^ n ∈ F as its q ^ n-th power.

theorem TauCeti.Place.relativeDegree_eq_one_of_isPurelyInseparable (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'] [IsPurelyInseparable F F'] (P' : Place k' F') [Algebra.IsSeparable (restrict k F P').ResidueField P'.ResidueField] : relativeDegree k F P' = 1

In a purely inseparable extension, a place with separable residue extension has relative degree one: the residue extension is then both separable and purely inseparable, hence trivial. The separability hypothesis holds in particular when the residue field of the place below is perfect.

theorem TauCeti.Place.ramificationIdx_eq_finrank_of_isPurelyInseparable (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'] [IsPurelyInseparable F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : IsFunctionField k F) (P' : Place k' F') [Algebra.IsSeparable (restrict k F P').ResidueField P'.ResidueField] : ramificationIdx F P' = Module.finrank F F'

In a finite purely inseparable extension of an algebraic function field, a place with separable residue extension is totally ramified: e(P' ∣ P) = [F' : F]. The separability hypothesis holds in particular when the residue field of the place below is perfect; without it the conclusion fails, see TauCeti.Place.ramificationIdx_adicOfIrreducible_X_pow_sub_C.

An unramified place of a purely inseparable extension

Let k have characteristic p and let s ∈ k not be a p-th power, so that x ^ p − s is irreducible. In k(x) over k(t), t = x ^ p, the place of x ^ p − s lies over the zero of t − s with ramification index 1 and relative degree p, although the extension is purely inseparable of degree p. The residue field k of the place below is not perfect.

theorem TauCeti.Place.ramificationIdx_adicOfIrreducible_X_pow_sub_C {k : Type u} [Field k] {p : ℕ} [Fact (Nat.Prime p)] [CharP k p] {s : k} (hs : ∀ (c : k), c ^ p ≠ s) : ramificationIdx (↥k⟮RatFunc.X ^ p⟯) (adicOfIrreducible ⋯) = 1

In k(x) / k(x ^ p), the place of x ^ p − s, for s not a p-th power, is unramified: e = 1, although the extension is purely inseparable of degree p.

theorem TauCeti.Place.ord_restrict_adicOfIrreducible_X_pow_sub_C {k : Type u} [Field k] {p : ℕ} [Fact (Nat.Prime p)] [CharP k p] {s : k} (hs : ∀ (c : k), c ^ p ≠ s) : (restrict k (↥k⟮RatFunc.X ^ p⟯) (adicOfIrreducible ⋯)).ord (IntermediateField.AdjoinSimple.gen k (RatFunc.X ^ p) - (algebraMap k ↥k⟮RatFunc.X ^ p⟯) s) = 1

In k(x) / k(x ^ p), the place of x ^ p − s, for s not a p-th power, lies over the zero of t − s, where t = x ^ p: the order of t − s at the place below is 1.

theorem TauCeti.Place.relativeDegree_adicOfIrreducible_X_pow_sub_C {k : Type u} [Field k] {p : ℕ} [Fact (Nat.Prime p)] [CharP k p] {s : k} (hs : ∀ (c : k), c ^ p ≠ s) : relativeDegree k (↥k⟮RatFunc.X ^ p⟯) (adicOfIrreducible ⋯) = p

In k(x) / k(x ^ p), the place of x ^ p − s, for s not a p-th power, has relative degree p: the whole degree of the purely inseparable extension is carried by the residue extension.