Automorphisms preserve Weierstrass gaps

An automorphism of a function field transports a function with order -n at P and nonnegative order elsewhere to one with the same property at the image of P. Thus pole numbers, gaps, and the finite set of gaps are invariant under the action on places. This is the invariance needed to make the exceptional Weierstrass places an invariant set.

The transport uses only the order functions at places; it needs no function-field or exact-constant hypothesis.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.6 and III.5.

theorem TauCeti.Place.IsPoleNumber.smul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (σ : Gal(F/k)) (P : Place k F) (n : ℕ) (h : P.IsPoleNumber n) : (σ • P).IsPoleNumber n

An automorphism carries each pole number at a place to the same pole number at its image.

@[simp]

theorem TauCeti.Place.isPoleNumber_smul_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (σ : Gal(F/k)) (P : Place k F) (n : ℕ) : (σ • P).IsPoleNumber n ↔ P.IsPoleNumber n

Pole numbers at the image of a place are precisely its original pole numbers.

theorem TauCeti.Place.isGap_smul_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (σ : Gal(F/k)) (P : Place k F) (n : ℕ) : (σ • P).IsGap n ↔ P.IsGap n

Gaps at the image of a place are precisely its original gaps.

@[simp]

theorem TauCeti.Place.gapNumbersUpTo_smul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (σ : Gal(F/k)) (P : Place k F) (m : ℕ) : (σ • P).gapNumbersUpTo m = P.gapNumbersUpTo m

The finite set of gaps up to any bound is unchanged by an automorphism.

@[simp]

theorem TauCeti.Place.weierstrassGaps_smul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (σ : Gal(F/k)) (P : Place k F) : (σ • P).weierstrassGaps = P.weierstrassGaps

The finite set of Weierstrass gaps is unchanged by an automorphism.