Theorems · Theorem · commutative algebra

RingHom.HoldsForLocalization.localRingHom

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => P) →
        ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {p : Ideal R} [inst_2 : p.IsPrime] {q : Ideal S}
          [inst_3 : q.IsPrime] {f : R →+* S} (h : p = Ideal.comap f q), P f → P (Localization.localRingHom p q f h)

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingIdeal.IsPrimeIdeal.IsPrime