{R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            {P' : Type u_3} →
              [inst_3 : CommRing P'] →
                [inst_4 : Algebra R P'] → (P →ₐ[R] P') → FractionalIdeal S P → FractionalIdeal S P'