Theorems · Theorem · commutative algebra

RingHom.RespectsIso.isLocalization_away_iff

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.RespectsIso P →
    ∀ {R S : Type u} (R' S' : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing R']
      [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] (f : R →+* S) (r : R)
      [inst_6 : IsLocalization.Away r R'] [inst_7 : IsLocalization.Away (f r) S'],
      P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)

Defined in

Mathlib.RingTheory.RingHomProperties

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRingAlgebraAlgebraIsLocalization.AwayIsLocalization.Away