Theorems · Theorem · commutative algebra

Localization.localRingHom_to_map

∀ {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) (hIJ : I = Ideal.comap f J) (x : R),
  (Localization.localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) =
    (algebraMap P (Localization.AtPrime J)) (f x)

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringIdeal.IsPrimeIdeal.IsPrime