The inertia group of a place, and the residue action of the decomposition group #
Let F' / F be a finite Galois extension of fields, k a subfield of F, and P a place of
F' / k. An automorphism in the decomposition group of P preserves the valuation ring 𝒪_P
and hence its maximal ideal, so it descends to an automorphism of the residue field F'_P; since
it fixes F pointwise it fixes the residue field F_{P ∩ F} of the place below, so the descent
is a homomorphism
TauCeti.Place.residueAut : G_Z(P) →* (F'_P ≃ₐ[F_{P ∩ F}] F'_P).
Its kernel is Mathlib's ValuationSubring.inertiaSubgroup, the inertia group of P.
The residue action distinguishes the automorphisms that become invisible after reduction from those detected on the residue field. Its surjectivity shows that every automorphism of the residue extension arises this way, so the inertia quotient captures exactly the residue-field symmetries and relates ramification to the separable and inseparable residue degrees.
Consequently G_Z(P) / G_T(P) is the automorphism group of the residue extension and of its
separable closure. Its order is the separable residue degree, while the inertia group has order
the ramification index times the inseparable residue degree. When the residue extension is
separable, these specialize to orders f(P ∣ P ∩ F) and e(P ∣ P ∩ F), respectively.
This is Stichtenoth, Definition 3.8.1 and the second half of Theorem 3.8.2; the first half — the
order of the decomposition group, and the decomposition field — is in
TauCeti/FieldTheory/FunctionField/Place/Extension/Decomposition.lean.
Main definitions #
TauCeti.Place.residueAut: the homomorphism from the decomposition group of a place to the automorphism group of the residue extension, withTauCeti.Place.residueAut_residuecomputing it on residues.TauCeti.Place.decompositionQuotientInertiaEquiv: the induced isomorphism of the decomposition group modulo the inertia group with the automorphism group of the residue extension, withTauCeti.Place.decompositionQuotientInertiaEquiv_mkcomputing it on classes.TauCeti.Place.decompositionQuotientInertiaEquivSeparableClosure: the corresponding identification with the automorphism group of the separable part of the residue extension.
Main results #
TauCeti.Place.ker_residueAut: the kernel ofTauCeti.Place.residueAutis the inertia group, restated elementwise asTauCeti.Place.mem_inertiaSubgroup_iff.TauCeti.Place.residueAut_surjective: the decomposition group surjects onto the automorphism group of the residue extension.TauCeti.Place.card_inertiaSubgroup_mul_card_residueFieldAut: the order of the inertia group times the order of the residue automorphism group ise · f.TauCeti.Place.card_decompositionQuotientInertia_eq_finSepDegreeandTauCeti.Place.card_inertiaSubgroup_eq_ramificationIdx_mul_finInsepDegree: the unconditional formulas|G_Z/G_T| = f_sepand|G_T| = e · f_ins.TauCeti.Place.normal_residueField: the residue extension at a place of a Galois extension is normal; henceTauCeti.Place.card_residueFieldAutandTauCeti.Place.card_inertiaSubgroup, which give the residue automorphism group orderf(P ∣ P ∩ F)and the inertia group ordere(P ∣ P ∩ F)once the residue extension is separable.TauCeti.Place.decompositionSubgroup_decompositionField_eq_top: over its decomposition field a place is fixed by the whole Galois group.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 3.8.1 and Theorem 3.8.2.
The decomposition group of P fixes the valuation ring of the place below P pointwise, so
its action on 𝒪_P is by 𝒪_{P ∩ F}-algebra automorphisms.
The induced action of the decomposition group on the residue field of P is by
F_{P ∩ F}-algebra automorphisms.
The residue action of the decomposition group (Stichtenoth, Theorem 3.8.2): an
automorphism of F' fixing the place P descends to an automorphism of the residue field F'_P
over the residue field of the place below P.
Equations
Instances For
The residue action, on residues (Stichtenoth, Theorem 3.8.2): the automorphism of F'_P
induced by g sends the residue of an element x of 𝒪_P to the residue of g x.
The inertia group, elementwise (Stichtenoth, Definition 3.8.1): an automorphism fixing P
lies in the inertia group exactly when it acts trivially on the residue field.
The inertia group is the kernel of the residue action (Stichtenoth, Theorem 3.8.2): this
identifies Mathlib's ValuationSubring.inertiaSubgroup, defined as the kernel of the action on
the residue field, with the kernel of TauCeti.Place.residueAut, which records that the action
is by automorphisms over the residue field of the place below.
The decomposition group surjects onto the automorphisms of the residue extension (Stichtenoth, Theorem 3.8.2).
The decomposition group modulo the inertia group is the automorphism group of the residue extension (Stichtenoth, Theorem 3.8.2).
Equations
Instances For
The isomorphism of TauCeti.Place.decompositionQuotientInertiaEquiv is induced by the residue
action: it sends the class of g to the residue automorphism of g.
The order of the inertia group, unconditionally (Stichtenoth, Theorem 3.8.2): together
with the residue automorphism group it accounts for the order e · f of the decomposition
group.
The residue extension at a place of a Galois extension is normal (Stichtenoth, Theorem 3.8.2).
Normality holds over the residue field of the decomposition field because the valuation ring of
P is an invariant extension there, and it descends to the residue field of F because the two
residue fields agree.
The residue automorphism group is the automorphism group of the separable part (Stichtenoth, Theorem 3.8.2). Restriction to the separable closure is an isomorphism because the remaining residue extension is purely inseparable.
Equations
Instances For
residueFieldAutEquivSeparableClosure acts by restricting a residue automorphism to the
separable closure.
The quotient of the decomposition group by inertia, identified with the automorphism group of the separable part of the residue extension (Stichtenoth, Theorem 3.8.2).
Equations
Instances For
On the separable closure, the separable-part quotient equivalence sends the class of g to
the residue automorphism of g.
The residue automorphism group has order equal to the separable residue degree (Stichtenoth, Theorem 3.8.2).
The decomposition group modulo inertia has order equal to the separable residue degree (Stichtenoth, Theorem 3.8.2).
The unconditional order of the inertia group (Stichtenoth, Theorem 3.8.2): it is the ramification index times the inseparable residue degree.
The residue automorphism group has order f(P ∣ P ∩ F) (Stichtenoth, Theorem 3.8.2),
when the residue extension is separable: it is then Galois, since it is always normal.
The inertia group has order e(P ∣ P ∩ F) (Stichtenoth, Theorem 3.8.2), when the residue
extension is separable.