Theorems · Definition · algebraic geometry

RingHom.SurjectiveOnStalks

{R : Type u_1} → [inst : CommRing R] → {S : Type u_2} → [inst_1 : CommRing S] → (R →+* S) → Prop

A ring homomorphism R →+* S is surjective on stalks if R_p →+* S_q is surjective for all pairs of primes p = f⁻¹(q).

Defined in

Mathlib.RingTheory.SurjectiveOnStalks

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommRingCommRing