The decomposition group and the decomposition field of a place

Let F' / F be a finite Galois extension of fields, k a subfield of F, and P a place of F' / k. The Galois group acts on the places of F' / k and is transitive on each fibre of restriction, so the fibre through P is the orbit of P and the stabilizer of P — Mathlib's ValuationSubring.decompositionSubgroup of the valuation ring of P — has index the number of places over P ∩ F. Comparing that count with the fundamental identity r · e · f = [F' : F] gives the order of the decomposition group, TauCeti.Place.card_decompositionSubgroup: it is e(P ∣ P ∩ F) · f(P ∣ P ∩ F).

The decomposition field Z of P is the subfield of F' fixed by that group. The Galois group of F' over Z is again the decomposition group, so every automorphism of F' over Z fixes P, and transitivity then forces P to be the only place of F' over its restriction to Z. With the fibre a single point, the fundamental identity over the decomposition field reads e(P ∣ P ∩ Z) · f(P ∣ P ∩ Z) = [F' : Z] = e(P ∣ P ∩ F) · f(P ∣ P ∩ F), and multiplicativity in the tower F ⊆ Z ⊆ F' then splits off e = f = 1 below Z: the whole of the ramification and of the residue extension of P over F happens over the decomposition field.

This is Stichtenoth, Definition 3.8.1 and the first half of Theorem 3.8.2. The second half — that the decomposition group surjects onto the automorphism group of the separable part of the residue extension, with kernel the inertia group ValuationSubring.inertiaSubgroup — is not proved here.

Main definitions

• TauCeti.Place.decompositionField: the subfield of F' fixed by the decomposition group of a place, an IntermediateField F F', with TauCeti.Place.mem_decompositionField_iff for its membership and TauCeti.Place.fixingSubgroup_decompositionField for the Galois correspondence it sits in: its fixing subgroup is the decomposition group again.

Main results

• TauCeti.Place.card_decompositionSubgroup: the decomposition group of P has order e(P ∣ P ∩ F) · f(P ∣ P ∩ F), and TauCeti.Place.finrank_decompositionField restates this as the degree of F' over the decomposition field.
• TauCeti.Place.eq_of_restrict_decompositionField_eq and TauCeti.Place.setOf_restrict_decompositionField_eq_eq_singleton: a place is the only place of F' above its restriction to its decomposition field.
• TauCeti.Place.ramificationIdx_restrict_decompositionField and TauCeti.Place.relativeDegree_restrict_decompositionField: below the decomposition field the ramification index and the relative degree are 1, so by TauCeti.Place.ramificationIdx_decompositionField and TauCeti.Place.relativeDegree_decompositionField both are unchanged above it.
• TauCeti.Place.decompositionSubgroup_decompositionField_eq_top: over its decomposition field a place is fixed by the whole Galois group.
• TauCeti.Place.decompositionSubgroup_integers_smul and TauCeti.Place.decompositionField_smul: conjugate places have conjugate decomposition groups and decomposition fields.
• TauCeti.Place.decompositionField_eq_top_iff_isSplitCompletely: the decomposition field is everything exactly when the place below splits completely.

References

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

theorem TauCeti.Place.card_decompositionSubgroup {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : Nat.card ↥(ValuationSubring.decompositionSubgroup F P.integers) = ramificationIdx F P * relativeDegree k F P

The order of the decomposition group (Stichtenoth, Theorem 3.8.2): the stabilizer of a place P in a finite Galois extension has order e(P ∣ P ∩ F) · f(P ∣ P ∩ F).

def TauCeti.Place.decompositionField {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') : IntermediateField F F'

The decomposition field of a place P of F' / k in a finite Galois extension F' / F (Stichtenoth, Definition 3.8.1): the subfield of F' fixed by the decomposition group of P.

Equations

• TauCeti.Place.decompositionField F P = IntermediateField.fixedField (ValuationSubring.decompositionSubgroup F P.integers)

@[simp]

theorem TauCeti.Place.mem_decompositionField_iff {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') (x : F') : x ∈ decompositionField F P ↔ ∀ σ ∈ ValuationSubring.decompositionSubgroup F P.integers, σ x = x

An element of F' lies in the decomposition field of P exactly when the decomposition group of P fixes it.

@[simp]

theorem TauCeti.Place.fixingSubgroup_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F'] [Algebra F F'] [FiniteDimensional F F'] (P : Place k F') : (decompositionField F P).fixingSubgroup = ValuationSubring.decompositionSubgroup F P.integers

The Galois correspondence for the decomposition field: the automorphisms of F' fixing the decomposition field of P pointwise are exactly the decomposition group of P.

@[simp]

theorem TauCeti.Place.restrictScalars_smul_eq_self {k : Type u} (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (P : Place k F') (τ : Gal(F'/↥(decompositionField F P))) : AlgEquiv.restrictScalars F τ • P = P

An automorphism of F' over the decomposition field of P, read as an automorphism over F, fixes P.

@[simp]

theorem TauCeti.Place.decompositionSubgroup_decompositionField_eq_top {k : Type u} (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (P : Place k F') : ValuationSubring.decompositionSubgroup (↥(decompositionField F P)) P.integers = ⊤

Over its decomposition field a place is fixed by the whole Galois group (Stichtenoth, Theorem 3.8.2): the decomposition group of P in F' / Z is everything, because the decomposition group of P in F' / F is by construction the Galois group of F' over Z.

theorem TauCeti.Place.eq_of_restrict_decompositionField_eq {k : Type u} (F : Type v) {F' : Type v'} [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'] {P Q : Place k F'} (h : restrict k (↥(decompositionField F P)) Q = restrict k (↥(decompositionField F P)) P) : Q = P

A place is the only place of F' above its restriction to its decomposition field (Stichtenoth, Theorem 3.8.2).

@[simp]

theorem TauCeti.Place.setOf_restrict_decompositionField_eq_eq_singleton {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : {Q : Place k F' | restrict k (↥(decompositionField F P)) Q = restrict k (↥(decompositionField F P)) P} = {P}

The fibre of a place over its restriction to its decomposition field is a single point.

theorem TauCeti.Place.finrank_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : Module.finrank (↥(decompositionField F P)) F' = ramificationIdx F P * relativeDegree k F P

The degree of F' over the decomposition field (Stichtenoth, Theorem 3.8.2): it is the order of the decomposition group, that is e(P ∣ P ∩ F) · f(P ∣ P ∩ F).

theorem TauCeti.Place.ramificationIdx_mul_relativeDegree_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : ramificationIdx (↥(decompositionField F P)) P * relativeDegree k (↥(decompositionField F P)) P = ramificationIdx F P * relativeDegree k F P

The product e · f is the same over the decomposition field as over F (Stichtenoth, Theorem 3.8.2): this is the form in which the fundamental identity over the decomposition field delivers it. That each of the two factors is separately unchanged is TauCeti.Place.ramificationIdx_decompositionField and TauCeti.Place.relativeDegree_decompositionField.

@[simp]

theorem TauCeti.Place.ramificationIdx_restrict_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : ramificationIdx F (restrict k (↥(decompositionField F P)) P) = 1

The restriction of a place to its decomposition field is unramified over F (Stichtenoth, Theorem 3.8.2): no ramification of P over F happens below the decomposition field.

@[simp]

theorem TauCeti.Place.relativeDegree_restrict_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : relativeDegree k F (restrict k (↥(decompositionField F P)) P) = 1

The residue extension below the decomposition field is trivial (Stichtenoth, Theorem 3.8.2): the restriction of P to its decomposition field has relative degree 1 over F.

@[simp]

theorem TauCeti.Place.ramificationIdx_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : ramificationIdx (↥(decompositionField F P)) P = ramificationIdx F P

The ramification index is unchanged over the decomposition field (Stichtenoth, Theorem 3.8.2).

@[simp]

theorem TauCeti.Place.relativeDegree_decompositionField {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : relativeDegree k (↥(decompositionField F P)) P = relativeDegree k F P

The relative degree is unchanged over the decomposition field (Stichtenoth, Theorem 3.8.2).

@[simp]

theorem TauCeti.Place.decompositionSubgroup_integers_smul {k : Type u} (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (P : Place k F') : ValuationSubring.decompositionSubgroup F (σ • P).integers = Subgroup.map (↑(MulAut.conj σ)) (ValuationSubring.decompositionSubgroup F P.integers)

The decomposition group of a conjugate place is the conjugate decomposition group (Stichtenoth, Theorem 3.8.2).

@[simp]

theorem TauCeti.Place.decompositionField_smul {k : Type u} (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] (σ : Gal(F'/F)) (P : Place k F') : decompositionField F (σ • P) = IntermediateField.map (↑σ) (decompositionField F P)

The decomposition field of a conjugate place is the image of the decomposition field (Stichtenoth, Theorem 3.8.2).

theorem TauCeti.Place.finrank_decompositionField_eq_ncard_setOf_restrict_eq {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : Module.finrank F ↥(decompositionField F P) = {Q : Place k F' | restrict k F Q = restrict k F P}.ncard

The degree of the decomposition field over F (Stichtenoth, Theorem 3.8.2): it is the number of places of F' / k lying over the place below P.

theorem TauCeti.Place.decompositionField_eq_top_iff_isSplitCompletely {k : Type u} (F : Type v) {F' : Type v'} [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'] (P : Place k F') : decompositionField F P = ⊤ ↔ (restrict k F P).IsSplitCompletely

A place splits completely exactly when its decomposition field is everything (Stichtenoth, Definition 3.1.13 and Theorem 3.8.2).