Theorems · Definition · ring theory

OreLocalization.universalMulHom

{R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {T : Type u_2} →
          [inst_2 : Monoid T] → (f : R →* T) → (fS : ↥S →* Tˣ) → (∀ (s : ↥S), f ↑s = ↑(fS s)) → OreLocalization S R →* T

The universal lift from a morphism R →* T, which maps elements of S to units of T, to a morphism R[S⁻¹] →* T.

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

4 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

MonoidOreLocalization.OreSetMonoid