Theorems · Definition · commutative algebra

IsLocalization.lift

{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)) → S →+* P

Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of CommSemirings g : R →+* P such that g y is invertible for all y : M, the homomorphism induced from S to P sending z : S to g x * (g y)⁻¹, where (x, y) : R × M are such that z = f x * (f y)⁻¹.

Defined in

Mathlib.RingTheory.Localization.Defs

Cited by

27 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringIsLocalization