Normalized fractions and change of coefficients

A rational function has a unique relatively prime numerator and monic denominator. Consequently, an embedding of coefficient fields carries its normalized numerator and denominator to those of the image. These compatibility results allow invariance of a rational function to be checked on its polynomial coefficients.

theorem RatFunc.num_denom_eq_of_isCoprime_of_monic {K : Type u_2} [Field K] {z : RatFunc K} {p q : Polynomial K} (hpq : IsCoprime p q) (hq : q.Monic) (hz : z = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) : z.num = p ∧ z.denom = q

A relatively prime numerator and monic denominator are the normalized fraction of a rational function.

@[simp]

theorem RatFunc.num_mapRingHom {F : Type u_1} {K : Type u_2} [Field F] [Field K] (f : F →+* K) (h : nonZeroDivisors (Polynomial F) ≤ Submonoid.comap (Polynomial.mapRingHom f) (nonZeroDivisors (Polynomial K))) (z : RatFunc F) : ((mapRingHom (Polynomial.mapRingHom f) h) z).num = Polynomial.map f z.num

Embedding the coefficient field commutes with taking the normalized numerator.

@[simp]

theorem RatFunc.denom_mapRingHom {F : Type u_1} {K : Type u_2} [Field F] [Field K] (f : F →+* K) (h : nonZeroDivisors (Polynomial F) ≤ Submonoid.comap (Polynomial.mapRingHom f) (nonZeroDivisors (Polynomial K))) (z : RatFunc F) : ((mapRingHom (Polynomial.mapRingHom f) h) z).denom = Polynomial.map f z.denom

Embedding the coefficient field commutes with taking the monic denominator.