Prime elements at a rational place above

Let F' / F be an integral extension, with F a field over k and F' a field over k', and let P' be a rational place of F' / k' lying over the place P of F / k with e(P' ∣ P) = 1. A prime element of P of the form q(z), with q separable over k and z regular at P, yields the prime element z - a of P', where a is the value of z at P'.

Main results

• TauCeti.Place.exists_ord_sub_algebraMap_eq_one_of_ord_aeval_eq_one: at a rational place P' unramified over P, a prime element q(z) of P with q separable yields a prime element z - a of P'.

theorem TauCeti.Place.exists_ord_sub_algebraMap_eq_one_of_ord_aeval_eq_one {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] {P' : Place k' F'} (hdeg : P'.degree = 1) (he : ramificationIdx F P' = 1) {z : F} (hz : 0 ≤ (restrict k F P').ord z) {q : Polynomial k} (hq : q.Separable) (hqz : (restrict k F P').ord ((Polynomial.aeval z) q) = 1) : ∃ (a : k'), P'.ord ((algebraMap F F') z - (algebraMap k' F') a) = 1

A prime element q(z) below gives a prime element z - a at a rational place above: at a rational place P' of F' over a place P of F with e(P' ∣ P) = 1, a prime element q(z) of P, with q separable over k and z regular at P, gives a prime element z - a of P' for some constant a, namely the value of z at P', which is a simple root of q.