Orders of polynomials in x at a place over a finite place of k(x)

Let F be a finite extension of the rational function field k(x). At a place P of F lying over the finite place of k(x) given by an irreducible polynomial q, the order of a nonzero polynomial in x is the ramification index of P over k(x) times the multiplicity of q in the polynomial.

Main results

• TauCeti.Place.ord_algebraMap_eq_of_restrict_eq: the order of a nonzero polynomial in x at a place over the finite place q.
• TauCeti.Place.ord_algebraMap_pos_of_restrict_eq: such a polynomial has positive order when it is divisible by q.

theorem TauCeti.Place.ord_algebraMap_eq_of_restrict_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] {q : Polynomial k} (hq : Irreducible q) {P : Place k F} (hP : restrict k (RatFunc k) P = adicOfIrreducible hq) {p : Polynomial k} (hp : p ≠ 0) : P.ord ((algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) p)) = ↑(ramificationIdx (RatFunc k) P) * ↑(multiplicity q p)

At a place over a finite place q of k(x), a nonzero polynomial in x has order e times its multiplicity at q, where e is the ramification index over k(x).

theorem TauCeti.Place.ord_algebraMap_pos_of_restrict_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] [Algebra.IsIntegral (RatFunc k) F] {q : Polynomial k} (hq : Irreducible q) {P : Place k F} (hP : restrict k (RatFunc k) P = adicOfIrreducible hq) {p : Polynomial k} (hp : p ≠ 0) (hdvd : q ∣ p) : 0 < P.ord ((algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) p))

A nonzero polynomial in x divisible by q has positive order at a place over the finite place q of k(x).