Theorems · Theorem · commutative algebra

IsLocalization.eq_of_eq

∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] {g : R →+* P},
  (∀ (y : ↥M), IsUnit (g ↑y)) → ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → g x = g y

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →+* P such that g(M) ⊆ Units P, f x = f y → g x = g y for all x y : R.

Defined in

Mathlib.RingTheory.Localization.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringIsLocalization