Theorems · Definition · field theory

RatFunc.map

{R : Type u_3} →
  {S : Type u_4} →
    {F : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : FunLike F (Polynomial R) (Polynomial S)] →
            [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)] →
              (φ : F) →
                nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S)) →
                  RatFunc R →* RatFunc S

Lift a monoid homomorphism that maps polynomials φ : R[X] →* S[X] to a R⟮X⟯ →* S⟮X⟯, on the condition that φ maps non-zero-divisors to non-zero-divisors, by mapping both the numerator and denominator and quotienting them.

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

8 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingFunLikeMonoidHomClass