Theorems · Theorem · commutative algebra

RingHom.locally_iff_finite

∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Defined in

Mathlib.RingTheory.RingHom.Locally

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRing