Theorems · Definition · group theory

Submonoid.LocalizationMap.AwayMap.lift

{M : Type u_1} →
  [inst : CommMonoid M] →
    {N : Type u_2} →
      [inst_1 : CommMonoid N] →
        {P : Type u_3} →
          [inst_2 : CommMonoid P] →
            {g : M →* P} → (x : M) → Submonoid.LocalizationMap.AwayMap x N → IsUnit (g x) → N →* P

Given x : M, a Localization map F : M →* N away from x, and a map of CommMonoids g : M →* P such that g x is invertible, the homomorphism induced from N to P sending z : N to g y * (g x)⁻ⁿ, where y : M, n : ℕ are such that z = F y * (F x)⁻ⁿ.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Away

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidCommMonoid