Theorems · Definition · commutative algebra

RingHom.Locally

({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] → (R →+* S) → Prop

For a property of ring homomorphisms P, Locally P holds for f : R →+* S if it holds locally on S, i.e. if there exists a subset { t } of S generating the unit ideal, such that P holds for all compositions R →+* Sₜ. We may require s to be finite here, for the equivalence, see locally_iff_finite.

Defined in

Mathlib.RingTheory.RingHom.Locally

Cited by

28 results in Mathlib

Foundations

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

Assumes

CommRingCommRing