Theorems · Theorem · commutative algebra

Localization.localRingHom_comp

∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  {S : Type u_4} [inst_2 : CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P) [hK : K.IsPrime] (f : R →+* S)
  (hIJ : I = Ideal.comap f J) (g : S →+* P) (hJK : J = Ideal.comap g K),
  Localization.localRingHom I K (g.comp f) ⋯ =
    (Localization.localRingHom J K g hJK).comp (Localization.localRingHom I J f hIJ)

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringIdeal.IsPrimeCommSemiringIdeal.IsPrimeIdeal.IsPrime