Theorems · Definition · group theory

AddSubmonoid.LocalizationMap.lift

{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} →
            [inst_2 : AddCommMonoid P] → S.LocalizationMap N → {g : M →+ P} → (∀ (y : ↥S), IsAddUnit (g ↑y)) → N →+ P

Given a localization map f : M →+ N for a submonoid S ⊆ M and a map of AddCommMonoids 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

23 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidAddCommMonoid