Coefficient maps of rational function fields

A field isomorphism σ : K ≃+* L induces the isomorphism K(X) ≃+* L(X) applying σ to the coefficients and fixing the variable X: the map of fraction fields induced by Polynomial.mapEquiv σ. It is the field-isomorphism counterpart of Mathlib's RatFunc.mapRingHom, and is how an automorphism of the constants, such as an element of an absolute Galois group, acts on the rational function field.

Main definitions

• TauCeti.RatFunc.mapRingEquiv: the coefficient map K(X) ≃+* L(X) of σ : K ≃+* L.

Main results

• TauCeti.RatFunc.mapRingEquiv_X and TauCeti.RatFunc.mapRingEquiv_C: it fixes X and acts on the constants by σ.
• TauCeti.RatFunc.coe_mapRingEquiv: as a function it is RatFunc.mapRingHom of Polynomial.mapRingHom σ.
• TauCeti.RatFunc.mapRingEquiv_refl, TauCeti.RatFunc.mapRingEquiv_symm and TauCeti.RatFunc.mapRingEquiv_trans: it is functorial in σ.
• TauCeti.apply_algebraMap_eq_of_mapRingEquiv and TauCeti.finrank_eq_of_mapRingEquiv: an isomorphism F ≃+* F' of extensions carrying K(X) onto L(X) by the coefficient map of σ carries K onto L along σ, and the two extensions have the same degree.
• TauCeti.algebraMap_ratFunc_algebraMap_polynomial: a K-algebra map K(X) → L(X) sending X to X maps a polynomial over K to the polynomial with its coefficients mapped to L.
• RatFunc.mapRingEquiv_algebraMap_ratFunc: for such an algebra map from K(X) to L(X), the coefficient map of an automorphism of L fixing the image of K fixes the image of K(X).
• RatFunc.mapRingHom_algebraMap: Mathlib's RatFunc.mapRingHom φ restricts to φ on polynomials.

noncomputable def TauCeti.RatFunc.mapRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) : RatFunc K ≃+* RatFunc L

The isomorphism K(X) ≃+* L(X) induced by a field isomorphism σ : K ≃+* L, applying σ to the coefficients and fixing X.

@[simp]

theorem TauCeti.RatFunc.mapRingEquiv_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) (p : Polynomial K) : (mapRingEquiv σ) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (Polynomial L) (RatFunc L)) (Polynomial.map (↑σ) p)

On polynomials, the coefficient map of σ is Polynomial.map σ.

theorem TauCeti.RatFunc.coe_mapRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) : ⇑(mapRingEquiv σ) = ⇑(RatFunc.mapRingHom (Polynomial.mapRingHom ↑σ) ⋯)

The coefficient map of σ is Mathlib's RatFunc.mapRingHom of Polynomial.mapRingHom σ.

@[simp]

theorem TauCeti.RatFunc.mapRingEquiv_X {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) : (mapRingEquiv σ) RatFunc.X = RatFunc.X

The coefficient map fixes the variable.

@[simp]

theorem TauCeti.RatFunc.mapRingEquiv_C {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) (c : K) : (mapRingEquiv σ) (RatFunc.C c) = RatFunc.C (σ c)

The coefficient map acts on the constants by σ.

theorem TauCeti.RatFunc.mapRingEquiv_algebraMap_const {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) (c : K) : (mapRingEquiv σ) ((algebraMap K (RatFunc K)) c) = (algebraMap L (RatFunc L)) (σ c)

The coefficient map carries the image of K in K(X) onto the image of L along σ.

@[simp]

theorem TauCeti.RatFunc.mapRingEquiv_refl {K : Type u_1} [Field K] : mapRingEquiv (RingEquiv.refl K) = RingEquiv.refl (RatFunc K)

The coefficient map of the identity is the identity.

@[simp]

theorem TauCeti.RatFunc.mapRingEquiv_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] (σ : K ≃+* L) : (mapRingEquiv σ).symm = mapRingEquiv σ.symm

The inverse of the coefficient map of σ is the coefficient map of σ⁻¹.

theorem TauCeti.RatFunc.mapRingEquiv_trans {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (σ : K ≃+* L) (τ : L ≃+* M) : mapRingEquiv (σ.trans τ) = (mapRingEquiv σ).trans (mapRingEquiv τ)

The coefficient map of a composite is the composite of the coefficient maps.

theorem TauCeti.RatFunc.isScalarTower_of_algebraMap_C {F : Type u_4} {K : Type u_5} [Field F] [Field K] [Algebra F K] [Algebra (RatFunc F) (RatFunc K)] (hC : ∀ (c : F), (algebraMap (RatFunc F) (RatFunc K)) (RatFunc.C c) = RatFunc.C ((algebraMap F K) c)) : IsScalarTower F (RatFunc F) (RatFunc K)

An algebra map between rational function fields that preserves the given map on constants is compatible with the coefficient-field scalar tower.

theorem TauCeti.apply_algebraMap_eq_of_mapRingEquiv {K : Type u_1} {L : Type u_2} {F : Type u_3} {F' : Type u_4} [Field K] [Field L] [Field F] [Field F'] [Algebra (RatFunc K) F] [Algebra (RatFunc L) F'] (σ : K ≃+* L) (τ : F ≃+* F') (hτ : ∀ (x : RatFunc K), τ ((algebraMap (RatFunc K) F) x) = (algebraMap (RatFunc L) F') ((RatFunc.mapRingEquiv σ) x)) [Algebra K F] [Algebra L F'] [IsScalarTower K (RatFunc K) F] [IsScalarTower L (RatFunc L) F'] (c : K) : τ ((algebraMap K F) c) = (algebraMap L F') (σ c)

An isomorphism τ : F ≃+* F' carrying K(X) onto L(X) by the coefficient map of σ carries the constants K onto L along σ.

theorem TauCeti.finrank_eq_of_mapRingEquiv {K : Type u_1} {L : Type u_2} {F : Type u_3} {F' : Type u_4} [Field K] [Field L] [Field F] [Field F'] [Algebra (RatFunc K) F] [Algebra (RatFunc L) F'] (σ : K ≃+* L) (τ : F ≃+* F') (hτ : ∀ (x : RatFunc K), τ ((algebraMap (RatFunc K) F) x) = (algebraMap (RatFunc L) F') ((RatFunc.mapRingEquiv σ) x)) : Module.finrank (RatFunc L) F' = Module.finrank (RatFunc K) F

An isomorphism τ : F ≃+* F' carrying K(X) onto L(X) by the coefficient map of σ preserves the degree: the degrees of F and F' over the rational function fields agree.

theorem TauCeti.algebraMap_ratFunc_algebraMap_polynomial {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra (RatFunc K) (RatFunc L)] [IsScalarTower K (RatFunc K) (RatFunc L)] (hX : (algebraMap (RatFunc K) (RatFunc L)) RatFunc.X = RatFunc.X) (f : Polynomial K) : (algebraMap (RatFunc K) (RatFunc L)) ((algebraMap (Polynomial K) (RatFunc K)) f) = (algebraMap (Polynomial L) (RatFunc L)) (Polynomial.map (algebraMap K L) f)

A K-algebra map K(X) → L(X) sending X to X maps a polynomial over K to the same polynomial with its coefficients read in L.

@[simp]

theorem RatFunc.mapRingHom_algebraMap {K : Type u_1} {R : Type u_2} [CommRing K] [IsDomain K] [CommRing R] [IsDomain R] (φ : Polynomial K →+* Polynomial R) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p : Polynomial K) : (mapRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (Polynomial R) (RatFunc R)) (φ p)

On polynomials, Mathlib's coefficient map RatFunc.mapRingHom φ is φ.

theorem RatFunc.mapRingEquiv_algebraMap_ratFunc {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra (RatFunc F) (RatFunc K)] [IsScalarTower F (RatFunc F) (RatFunc K)] (hX : (algebraMap (RatFunc F) (RatFunc K)) X = X) {σ : K ≃+* K} (hσ : ∀ (c : F), σ ((algebraMap F K) c) = (algebraMap F K) c) (w : RatFunc F) : (TauCeti.RatFunc.mapRingEquiv σ) ((algebraMap (RatFunc F) (RatFunc K)) w) = (algebraMap (RatFunc F) (RatFunc K)) w

A coefficient automorphism of K(X) whose automorphism σ of K fixes the image of F fixes the image of F(X), for any F-algebra map F(X) → K(X) sending X to X.