Theorems · Definition · commutative algebra

Localization.localRingHom

{R : Type u_1} →
  [inst : CommSemiring R] →
    {P : Type u_3} →
      [inst_1 : CommSemiring P] →
        (I : Ideal R) →
          [hI : I.IsPrime] →
            (J : Ideal P) →
              [inst_2 : J.IsPrime] →
                (f : R →+* P) → I = Ideal.comap f J → Localization.AtPrime I →+* Localization.AtPrime J

For a ring hom f : R →+* S and a prime ideal J in S, the induced ring hom from the localization of R at J.comap f to the localization of S at J. To make this definition more flexible, we allow any ideal I of R as input, together with a proof that I = J.comap f. This can be useful when I is not definitionally equal to J.comap f.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

54 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringIdeal.IsPrimeIdeal.IsPrime