Unramified places in composita and Galois closures

A place P of F / k is unramified in an algebraic extension F' / k' when some place of F' lies above it and every place P' of F' above it has ramification index e(P' ∣ P) = 1 and separable residue extension F'_{P'} / F_P. Over a perfect residue field the separability condition is automatic, and this is Stichtenoth's notion (Definition 3.1.13). In general it cannot be dropped. Over 𝔽_p(s)(t), the Artin–Schreier extensions y^p - y = s t^{-p} and y^p - y = (s + t) t^{-p} both have e = 1 at t = 0, with residue extension 𝔽_p(s^{1/p}) / 𝔽_p(s). Their compositum contains a root of y^p - y = -t^{1 - p}, so it is ramified there.

In a finite Galois extension M / F, the restriction of a place Q of M to an intermediate field E is unramified over F exactly when E lies in the inertia field of Q (TauCeti.Place.le_inertiaField_iff). This file draws the two consequences of Stichtenoth's Corollary 3.9.3, for arbitrary residue fields. The fixing subgroup of a compositum is the intersection of the fixing subgroups, so a place is unramified in E₁ E₂ exactly when it is unramified in E₁ and in E₂. The Galois group permutes the places above P and carries their inertia fields along (TauCeti.Place.inertiaField_smul), so a place unramified in E is unramified in every conjugate of E, hence in the Galois closure of E, which those conjugates generate. Every finite separable extension of F embeds into a finite Galois one, and unramifiedness is invariant under isomorphism over F (TauCeti.Place.isUnramified_iff_of_algEquiv), so these statements cover the composita and Galois closures of finite separable extensions. This transport through a finite Galois overfield follows the proof of TauCeti.Place.isSplitCompletely_sup_iff in TauCeti/FieldTheory/FunctionField/Place/Extension/Splitting/Compositum.lean.

Ramification indices multiply in a tower F₀ ⊆ F₁ ⊆ F₂, and residue extensions are separable for the whole tower exactly when they are for both steps (TauCeti.Place.ramificationIdx_restrict_mul and its companions in TauCeti/FieldTheory/FunctionField/Place/Extension/Tower.lean). So a place of F₀ is unramified in F₂ exactly when it is unramified in F₁ and every place of F₁ above it is unramified in F₂. The branch places of an extension are the places that are not unramified in it; for finite maps of curves f : X → Y and g : Y → Z the tower statement reads Branch(g ∘ f) = g(Branch f) ∪ Branch g.

Main definitions

• TauCeti.Place.IsUnramified: a place is unramified in an extension, with the characteristic property TauCeti.Place.isUnramified_iff and the projections IsUnramified.exists_restrict_eq, IsUnramified.ramificationIdx_eq_one and IsUnramified.isSeparable.
• TauCeti.Place.branchPlaces: the places of the base field that are not unramified in an extension.

Main results

• TauCeti.Place.not_isUnramified_of_degree_eq_one: a place of degree one is not unramified once the constants contain a purely inseparable element outside k, whatever the ramification indices are.
• TauCeti.Place.isUnramified_iff_of_algEquiv: unramifiedness is invariant under an isomorphism of the upstairs field over the base field.
• TauCeti.Place.isUnramified_tower_iff: a place is unramified in a tower exactly when it is unramified in the lower step and every place above it is unramified in the upper step.
• TauCeti.Place.branchPlaces_eq_image_union: the branch places of a tower are the branch places of the lower step together with the places below the branch places of the upper step.
• TauCeti.Place.isUnramified_iff_forall_le_inertiaField: a place is unramified in E exactly when E lies in the inertia field of every place of M above it.
• TauCeti.Place.isUnramified_sup_iff: a place is unramified in a compositum of finite separable extensions exactly when it is unramified in both constituents.
• TauCeti.Place.isUnramified_normalClosure_iff: a place is unramified in the Galois closure of E exactly when it is unramified in E.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.1.6, Definition 3.1.13 and Corollary 3.9.3.

def TauCeti.Place.IsUnramified {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) : Prop

A place P of F / k is unramified in F' / k' when it has a place P' of F' above it, and every such P' has ramification index e(P' ∣ P) = 1 and a separable residue extension F'_{P'} / F_P (Stichtenoth, Definition 3.1.13, where the residue extensions are separable because the constant field is perfect). The existence clause keeps the predicate from holding vacuously when no place of F' / k' lies above P, for instance when k' = F' = F.

theorem TauCeti.Place.isUnramified_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 F F'] (P : Place k F) : P.IsUnramified ↔ (∃ (P' : Place k' F'), restrict k F P' = P) ∧ ∀ (P' : Place k' F'), restrict k F P' = P → ramificationIdx F P' = 1 ∧ Algebra.IsSeparable (restrict k F P').ResidueField P'.ResidueField

The characteristic property of an unramified place.

theorem TauCeti.Place.IsUnramified.exists_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'] [Algebra.IsIntegral F F'] {P : Place k F} (hP : P.IsUnramified) : ∃ (P' : Place k' F'), restrict k F P' = P

An unramified place has a place above it.

theorem TauCeti.Place.IsUnramified.ramificationIdx_eq_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'] [Algebra.IsIntegral F F'] {P : Place k F} (hP : P.IsUnramified) {P' : Place k' F'} (hP' : restrict k F P' = P) : ramificationIdx F P' = 1

A place above an unramified place has ramification index one.

theorem TauCeti.Place.IsUnramified.isSeparable {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} (hP : P.IsUnramified) {P' : Place k' F'} (hP' : restrict k F P' = P) : Algebra.IsSeparable (restrict k F P').ResidueField P'.ResidueField

A place above an unramified place has a separable residue extension.

def TauCeti.Place.branchPlaces {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'] : Set (Place k F)

The branch places of F' / k' over F / k: the places of F that are not unramified in F'. When every place of F lies below a place of F', as for a finite extension of function fields, these are the places of F lying below a place of F' with ramification index greater than one or with an inseparable residue extension. When moreover the residue fields have characteristic zero, only the ramification index matters.

@[simp]

theorem TauCeti.Place.mem_branchPlaces_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 F F'] {P : Place k F} : P ∈ branchPlaces k' F' ↔ ¬P.IsUnramified

theorem TauCeti.Place.not_isUnramified_of_degree_eq_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'] [Algebra.IsIntegral F F'] {P : Place k F} (hP : P.degree = 1) (q : ℕ) [ExpChar k q] {α : k'} (hα : α ∉ (algebraMap k k').range) {n : ℕ} (hn : α ^ q ^ n ∈ (algebraMap k k').range) : ¬P.IsUnramified

A rational place is not unramified in a purely inseparable extension of constants: if P has degree one and k' contains α ∉ k with α ^ (q ^ n) ∈ k, then P is not unramified in F' / k', whatever the ramification indices are.

theorem TauCeti.Place.isUnramified_iff_of_algEquiv {k : Type u_1} {F : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field F] [Field L] [Field L'] [Algebra k F] [Algebra k L] [Algebra k L'] [Algebra F L] [Algebra F L'] [IsScalarTower k F L] [IsScalarTower k F L'] [Algebra.IsIntegral F L] [Algebra.IsIntegral F L'] (P : Place k F) (e : L ≃ₐ[F] L') : P.IsUnramified ↔ P.IsUnramified

Unramifiedness depends only on the extension: it is invariant under an isomorphism of the upstairs field over the base field. This moves a finite separable extension into a finite Galois overfield without changing which places are unramified in it.

theorem TauCeti.Place.isUnramified_tower_iff {k₀ : Type u_1} {k₁ : Type u_2} {k₂ : Type u_3} {F₀ : Type u_4} {F₁ : Type u_5} {F₂ : Type u_6} [Field k₀] [Field k₁] [Field k₂] [Field F₀] [Field F₁] [Field F₂] [Algebra k₀ k₁] [Algebra k₁ k₂] [Algebra k₀ k₂] [Algebra F₀ F₁] [Algebra F₁ F₂] [Algebra F₀ F₂] [IsScalarTower F₀ F₁ F₂] [Algebra k₀ F₀] [Algebra k₁ F₁] [Algebra k₂ F₂] [Algebra k₀ F₁] [Algebra k₁ F₂] [Algebra k₀ F₂] [IsScalarTower k₀ k₁ F₁] [IsScalarTower k₁ k₂ F₂] [IsScalarTower k₀ F₀ F₁] [IsScalarTower k₁ F₁ F₂] [IsScalarTower k₀ k₂ F₂] [IsScalarTower k₀ F₀ F₂] [Algebra.IsIntegral F₀ F₁] [Algebra.IsIntegral F₁ F₂] [Algebra.IsIntegral F₀ F₂] [Algebra.IsIntegral k₁ k₂] (hF₂ : IsFunctionField k₂ F₂) (P : Place k₀ F₀) : P.IsUnramified ↔ P.IsUnramified ∧ ∀ (P₁ : Place k₁ F₁), restrict k₀ F₀ P₁ = P → P₁.IsUnramified

Unramifiedness in a tower (Stichtenoth, Proposition 3.1.6 and Definition 3.1.13): for a tower F₀ ⊆ F₁ ⊆ F₂, a place P of F₀ is unramified in F₂ exactly when it is unramified in F₁ and every place of F₁ above it is unramified in F₂.

The function-field hypothesis on F₂ provides a place of F₂ above every place of F₁.

theorem TauCeti.Place.branchPlaces_eq_image_union {k₀ : Type u_1} {k₁ : Type u_2} {k₂ : Type u_3} {F₀ : Type u_4} {F₁ : Type u_5} {F₂ : Type u_6} [Field k₀] [Field k₁] [Field k₂] [Field F₀] [Field F₁] [Field F₂] [Algebra k₀ k₁] [Algebra k₁ k₂] [Algebra k₀ k₂] [Algebra F₀ F₁] [Algebra F₁ F₂] [Algebra F₀ F₂] [IsScalarTower F₀ F₁ F₂] [Algebra k₀ F₀] [Algebra k₁ F₁] [Algebra k₂ F₂] [Algebra k₀ F₁] [Algebra k₁ F₂] [Algebra k₀ F₂] [IsScalarTower k₀ k₁ F₁] [IsScalarTower k₁ k₂ F₂] [IsScalarTower k₀ F₀ F₁] [IsScalarTower k₁ F₁ F₂] [IsScalarTower k₀ k₂ F₂] [IsScalarTower k₀ F₀ F₂] [Algebra.IsIntegral F₀ F₁] [Algebra.IsIntegral F₁ F₂] [Algebra.IsIntegral F₀ F₂] [Algebra.IsIntegral k₁ k₂] (hF₂ : IsFunctionField k₂ F₂) : branchPlaces k₂ F₂ = (fun (P₁ : Place k₁ F₁) => restrict k₀ F₀ P₁) '' branchPlaces k₂ F₂ ∪ branchPlaces k₁ F₁

Branch places of a tower: for a tower F₀ ⊆ F₁ ⊆ F₂, the branch places of F₂ / F₀ are the branch places of F₁ / F₀ together with the places of F₀ below the branch places of F₂ / F₁. For finite maps of curves f : X → Y and g : Y → Z this is the formula Branch(g ∘ f) = g(Branch f) ∪ Branch g.

theorem TauCeti.Place.isUnramified_iff_forall_le_inertiaField {k : Type u} {F : Type v} {M : Type w} [Field k] [Field F] [Field M] [Algebra k F] [Algebra k M] [Algebra F M] [IsScalarTower k F M] [FiniteDimensional F M] [IsGalois F M] (hF : IsFunctionField k F) (P : Place k F) (E : IntermediateField F M) : P.IsUnramified ↔ ∀ (Q : Place k M), restrict k F Q = P → E ≤ inertiaField F Q

A place is unramified in an intermediate field E of a finite Galois extension M exactly when E lies in the inertia field of every place of M above it.

@[simp]

theorem TauCeti.Place.isUnramified_sup_iff {k : Type u} {F : Type v} {M : Type w} [Field k] [Field F] [Field M] [Algebra k F] [Algebra k M] [Algebra F M] [IsScalarTower k F M] (hF : IsFunctionField k F) (P : Place k F) (E₁ E₂ : IntermediateField F M) [FiniteDimensional F ↥E₁] [FiniteDimensional F ↥E₂] [Algebra.IsSeparable F ↥E₁] [Algebra.IsSeparable F ↥E₂] : P.IsUnramified ↔ P.IsUnramified ∧ P.IsUnramified

Unramifiedness in a compositum (Stichtenoth, Corollary 3.9.3): a place is unramified in the compositum of two finite separable intermediate fields of M / F exactly when it is unramified in each of them. The ambient extension M / F need not be finite or separable.

@[simp]

theorem TauCeti.Place.isUnramified_normalClosure_iff {k : Type u} {F : Type v} {M : Type w} [Field k] [Field F] [Field M] [Algebra k F] [Algebra k M] [Algebra F M] [IsScalarTower k F M] [FiniteDimensional F M] [IsGalois F M] (hF : IsFunctionField k F) (P : Place k F) (E : IntermediateField F M) : P.IsUnramified ↔ P.IsUnramified

Unramifiedness in a Galois closure (Stichtenoth, Corollary 3.9.3): a place is unramified in the normal closure of an intermediate field E of a finite Galois extension M / F exactly when it is unramified in E.