Transporting places of the rational function field along the coefficient map

A field isomorphism σ : k ≃+* k' induces the coefficient map RatFunc.mapRingEquiv σ : k(t) ≃+* k'(t), and hence a bijection TauCeti.Place.equivOfRingEquiv σ (RatFunc.mapRingEquiv σ) _ between the places of k(t) and those of k'(t). This file computes that bijection on the degree-one finite places.

Main results

• TauCeti.Place.equivOfRingEquiv_mapRingEquiv_adicOfIrreducible_X_sub_C: the bijection carries the place t = a to the place t = σ a.

@[simp]

theorem TauCeti.Place.equivOfRingEquiv_mapRingEquiv_adicOfIrreducible_X_sub_C {k : Type u_1} {k' : Type u_2} [Field k] [Field k'] (σ : k ≃+* k') (a : k) : (equivOfRingEquiv σ (RatFunc.mapRingEquiv σ) ⋯) (adicOfIrreducible ⋯) = adicOfIrreducible ⋯

The coefficient map moves the place t = a to the place t = σ a: the bijection between the places of k(t) and those of k'(t) induced by the coefficient map of σ : k ≃+* k' carries the zero of t - a to the zero of t - σ a.