Theorems · Definition · group theory

Submonoid.LocalizationMap.lift

{M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} →
            [inst_2 : CommMonoid P] → S.LocalizationMap N → {g : M →* P} → (∀ (y : ↥S), IsUnit (g ↑y)) → N →* P

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

Defined in

Mathlib.GroupTheory.MonoidLocalization.Maps

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidCommMonoid