Theorems · Definition · field theory

RatFunc.mapRingHom

{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 : RingHomClass F (Polynomial R) (Polynomial S)] →
              (φ : F) →
                nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S)) →
                  RatFunc R →+* RatFunc S

Lift a ring 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

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingFunLikeRingHomClass