The Galois action on the places lying over a place

Let F' / F be an extension of fields and let k be a subfield of F. An F-automorphism σ of F' transports the places of F' / k: the valuation v_P ∘ σ⁻¹ is again normalized and trivial on the constants, so σ • P is a place, and v_{σ • P} (σ x) = v_P x. Since σ fixes F pointwise, σ • P lies over the same place of F / k as P does, with the same ramification index and the same relative degree.

The main theorem is that when F' / F is a finite Galois extension this action is transitive on each fibre: two places of F' / k lie over the same place of F / k exactly when one is carried to the other by an automorphism (Stichtenoth, Theorem 3.7.1). The proof is the classical one: weak approximation produces a function z with a zero at one of the two places and no zero or pole anywhere on either orbit, and the norm N_{F'/F} (z) = ∏ σ, σ z — an element of F — then has order 0 at one place of the fibre and order > 0 at another, which is impossible because on F the order at a place of F' is a positive multiple of the order at the place below.

Consequently the ramification index and the relative degree are constant on a fibre, and the fundamental identity of TauCeti/FieldTheory/FunctionField/Place/Extension/Fundamental.lean — which applies because a Galois extension is separable — takes the product form r · e · f = [F' : F] (Stichtenoth, Corollary 3.7.2). The stabilizer of a place is the decomposition group, and is identified with Mathlib's ValuationSubring.decompositionSubgroup.

Main definitions

• the MulAction (F' ≃ₐ[F] F') (Place k F') instance: the action of the automorphism group of F' / F on the places of F' / k, with TauCeti.Place.valuation_smul its defining property and TauCeti.Place.integers_smul the induced action on valuation rings.

Main results

• TauCeti.Place.restrictScalars_smul: the automorphisms of F' over an intermediate field of F' / F act on the places of F' / k through the action of the automorphisms over F.
• TauCeti.Place.valuation_apply_sub_lt_one_of_smul_eq_of_degree_eq_one: an automorphism fixing a rational place has the same residue on every regular function at that place.
• TauCeti.Place.degree_smul: the action preserves the degree of a place over the constants.
• TauCeti.Place.restrict_smul, TauCeti.Place.ramificationIdx_smul and TauCeti.Place.relativeDegree_smul: the action preserves the fibres of TauCeti.Place.restrict and the two invariants attached to a place of a fibre.
• TauCeti.Place.exists_smul_eq_of_restrict_eq and the packaged TauCeti.Place.restrict_eq_iff_exists_smul_eq: the Galois group acts transitively on the places over a place (Stichtenoth, Theorem 3.7.1), with TauCeti.Place.setOf_restrict_eq_eq_orbit restating a fibre as an orbit.
• TauCeti.Place.ramificationIdx_eq_of_restrict_eq and TauCeti.Place.relativeDegree_eq_of_restrict_eq: e and f are constant on a fibre, whence TauCeti.Place.ncard_mul_ramificationIdx_mul_relativeDegree_eq_finrank, the product form r · e · f = [F' : F] of the fundamental identity (Stichtenoth, Corollary 3.7.2).
• TauCeti.Place.ramificationIdxIn: the common ramification index of the places over a place of F, zero exactly on an empty fibre (TauCeti.Place.ramificationIdxIn_eq_zero_iff) and positive for an extension of function fields (TauCeti.Place.ramificationIdxIn_pos), with TauCeti.Place.ramificationIdxIn_mul_sum_fibre_eq summing e - 1 over a fibre: ∑_{P' ∣ P} (e(P' ∣ P) - 1) · deg P' = [F' : F] · (1 - 1/e) · deg P, cleared of the division.
• TauCeti.Place.stabilizer_eq_decompositionSubgroup: the stabilizer of a place is the decomposition group of its valuation ring, and TauCeti.Place.ncard_mul_card_stabilizer_eq_finrank is the orbit--stabilizer count of a fibre.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.7.

@[instance_reducible]

instance TauCeti.Place.instMulActionAlgEquiv {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'] : MulAction Gal(F'/F) (Place k F')

The action of the automorphism group of F' / F on the places of F' / k: an F-automorphism σ carries a place P to the place σ • P whose valuation is v_P ∘ σ⁻¹. Normalization is preserved because σ is bijective, and triviality on the constants because σ fixes F, hence k, pointwise.

Equations

• TauCeti.Place.instMulActionAlgEquiv = { smul := fun (σ : Gal(F'/F)) (P : TauCeti.Place k F') => TauCeti.Place.map (AlgEquiv.restrictScalars k σ) P, mul_smul := ⋯, one_smul := ⋯ }

theorem TauCeti.Place.smul_eq_map {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') : σ • P = map (AlgEquiv.restrictScalars k σ) P

The action is transport along the automorphism: σ • P is the place obtained from P by transport along σ, viewed as a k-algebra isomorphism of F' with itself.

@[simp]

theorem TauCeti.Place.valuation_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') (x : F') : (σ • P).valuation x = P.valuation (σ.symm x)

The defining property of the action: the valuation of σ • P is the valuation of P composed with σ⁻¹.

theorem TauCeti.Place.valuation_smul_apply {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') (x : F') : (σ • P).valuation (σ x) = P.valuation x

The action moves the valuation along σ.

theorem TauCeti.Place.valuation_apply_sub_lt_one_of_smul_eq_of_degree_eq_one {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') (hσ : σ • P = P) (hP : P.degree = 1) {z : F'} (hz : z ∈ P.integers) : P.valuation (σ z - z) < 1

An automorphism fixing a rational place has the same residue on regular functions: if σ fixes the place P of degree one, then σ z and z have the same residue at P for every z regular at P, that is, v_P (σ z - z) < 1.

@[simp]

theorem TauCeti.Place.ord_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') (x : F') : (σ • P).ord x = P.ord (σ.symm x)

The order function of σ • P is the order function of P composed with σ⁻¹.

theorem TauCeti.Place.ord_smul_apply {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') (x : F') : (σ • P).ord (σ x) = P.ord x

The action moves the order function along σ.

theorem TauCeti.Place.mem_integers_smul_iff {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') {x : F'} : x ∈ (σ • P).integers ↔ σ.symm x ∈ P.integers

Membership in the valuation ring of σ • P, read off at P.

theorem TauCeti.Place.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') : (σ • P).integers = σ • P.integers

The valuation ring of σ • P is the image of the valuation ring of P under σ, for Mathlib's pointwise action on valuation subrings.

@[simp]

theorem TauCeti.Place.restrictScalars_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'] (E : IntermediateField F F') (τ : Gal(F'/↥E)) (Q : Place k F') : AlgEquiv.restrictScalars F τ • Q = τ • Q

The two actions on places agree: restricting the scalars of an automorphism of F' over an intermediate field E down to F does not change the place it produces.

theorem TauCeti.Place.stabilizer_eq_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'] (P : Place k F') : MulAction.stabilizer Gal(F'/F) P = ValuationSubring.decompositionSubgroup F P.integers

The stabilizer of a place is the decomposition group of its valuation ring (Stichtenoth, Definition 3.8.1).

@[simp]

theorem TauCeti.Place.valuation_decompositionSubgroup_apply {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'] (P : Place k F') (g : ↥(ValuationSubring.decompositionSubgroup F P.integers)) (x : F') : P.valuation (↑g x) = P.valuation x

An automorphism fixing P leaves the valuation at P unchanged.

@[simp]

theorem TauCeti.Place.ord_decompositionSubgroup_apply {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'] (P : Place k F') (g : ↥(ValuationSubring.decompositionSubgroup F P.integers)) (x : F') : P.ord (↑g x) = P.ord x

An automorphism fixing P leaves the order at P unchanged.

theorem TauCeti.Place.mem_integers_decompositionSubgroup_apply {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'] (P : Place k F') (g : ↥(ValuationSubring.decompositionSubgroup F P.integers)) {x : F'} : ↑g x ∈ P.integers ↔ x ∈ P.integers

An automorphism fixing P preserves the valuation ring of P.

@[simp]

theorem TauCeti.Place.degree_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') : (σ • P).degree = P.degree

The action preserves the degree of a place: it is transport along σ, which identifies the residue fields of P and σ • P as k-algebras.

@[simp]

theorem TauCeti.Place.restrict_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'] [Algebra.IsIntegral F F'] (σ : Gal(F'/F)) (P : Place k F') : restrict k F (σ • P) = restrict k F P

The action preserves the fibres of restriction: σ • P lies over the same place of F / k as P does, because σ fixes F pointwise.

@[simp]

theorem TauCeti.Place.ramificationIdx_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'] [Algebra.IsIntegral F F'] (σ : Gal(F'/F)) (P : Place k F') : ramificationIdx F (σ • P) = ramificationIdx F P

The ramification index is invariant under the action.

@[simp]

theorem TauCeti.Place.relativeDegree_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'] [Algebra.IsIntegral F F'] (σ : Gal(F'/F)) (P : Place k F') : relativeDegree k F (σ • P) = relativeDegree k F P

The relative degree is invariant under the action: σ⁻¹ induces an isomorphism of the residue field of σ • P with the residue field of P over the residue field of the place below, which is the same for both.

theorem TauCeti.Place.exists_smul_eq_of_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 Q : Place k F'} (h : restrict k F P = restrict k F Q) : ∃ (σ : Gal(F'/F)), σ • P = Q

The Galois group acts transitively on the places over a place (Stichtenoth, Theorem 3.7.1): if two places of F' / k lie over the same place of F / k, then some F-automorphism of F' carries one to the other.

theorem TauCeti.Place.restrict_eq_iff_exists_smul_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'} : restrict k F P = restrict k F Q ↔ ∃ (σ : Gal(F'/F)), σ • P = Q

The fibres of restriction are the orbits of the Galois group (Stichtenoth, Theorem 3.7.1).

theorem TauCeti.Place.setOf_restrict_eq_eq_orbit {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 F Q = restrict k F P} = MulAction.orbit Gal(F'/F) P

The places lying over the place below P are exactly the places in the orbit of P.

theorem TauCeti.Place.ncard_mul_card_stabilizer_eq_finrank {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 F Q = restrict k F P}.ncard * Nat.card ↥(MulAction.stabilizer Gal(F'/F) P) = Module.finrank F F'

Orbit--stabilizer for the places over a place: the number of places of F' / k lying over the place below P, times the order of the stabilizer of P, is [F' : F].

theorem TauCeti.Place.ramificationIdx_eq_of_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 Q : Place k F'} (h : restrict k F P = restrict k F Q) : ramificationIdx F P = ramificationIdx F Q

The ramification index is constant on a fibre (Stichtenoth, Corollary 3.7.2).

theorem TauCeti.Place.relativeDegree_eq_of_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 Q : Place k F'} (h : restrict k F P = restrict k F Q) : relativeDegree k F P = relativeDegree k F Q

The relative degree is constant on a fibre (Stichtenoth, Corollary 3.7.2).

theorem TauCeti.Place.ncard_mul_ramificationIdx_mul_relativeDegree_eq_finrank {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 F Q = restrict k F P}.ncard * (ramificationIdx F P * relativeDegree k F P) = Module.finrank F F'

The fundamental identity in product form (Stichtenoth, Corollary 3.7.2): for a finite Galois extension the r places over a place all share one ramification index e and one relative degree f, and r · e · f = [F' : F].

A Galois extension is separable, so the fundamental identity applies with no further hypothesis.

noncomputable def TauCeti.Place.ramificationIdxIn {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) (F' : Type v') [Field F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [FiniteDimensional F F'] : ℕ

The ramification index of a place of the base in a Galois extension: all the places of F' over P share one ramification index (TauCeti.Place.ramificationIdx_eq_of_restrict_eq), and this is it. It is 0 when no place of F' lies over P, which does not happen for an extension of function fields (TauCeti.Place.restrict_surjective_of_finiteDimensional). This is the analogue for places of Mathlib's Ideal.ramificationIdxIn.

Equations

• P.ramificationIdxIn F' = if h : ∃ (P' : TauCeti.Place k F'), TauCeti.Place.restrict k F P' = P then TauCeti.Place.ramificationIdx F h.choose else 0

theorem TauCeti.Place.ramificationIdxIn_eq_ramificationIdx {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} {P' : Place k F'} (hP' : restrict k F P' = P) : P.ramificationIdxIn F' = ramificationIdx F P'

The ramification index of a place of the base is the ramification index of any place above it.

@[simp]

theorem TauCeti.Place.ramificationIdxIn_eq_zero_iff {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} : P.ramificationIdxIn F' = 0 ↔ ∀ (P' : Place k F'), restrict k F P' ≠ P

The ramification index of a place of the base vanishes exactly when no place lies above it.

theorem TauCeti.Place.ramificationIdxIn_pos {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'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {P : Place k F} : 0 < P.ramificationIdxIn F'

The ramification index of a place of the base is positive for an extension of function fields: some place of F' lies above it.

theorem TauCeti.Place.ramificationIdxIn_mul_sum_fibre_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} {P' : Place k F'} (hP' : restrict k F P' = P) : ↑(P.ramificationIdxIn F') * ∑ Q ∈ ⋯.toFinset, (↑(ramificationIdx F Q) - 1) * ↑Q.degree = ↑(Module.finrank F F') * ((↑(P.ramificationIdxIn F') - 1) * ↑P.degree)

The branch contribution of a Galois fibre: the places over a place P of F share one ramification index e and one relative degree f, and there are [F' : F] / (e f) of them, so

∑_{P' ∣ P} (e(P' ∣ P) - 1) · deg P' = [F' : F] · (1 - 1/e) · deg P.

This is that identity multiplied by e, which clears the division. Summed over the places of F it turns the degree of the tame different into the branch data (γ; e₁, …, e_r) of F' / F, whose deficit the Hurwitz bound is about.