Theorems · Definition · group theory

Submonoid.LocalizationMap.sec

{M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → S.LocalizationMap N → N → M × ↥S

Given a localization map f : M →* N, a section function sending z : N to some (x, y) : M × S such that f x * (f y)⁻¹ = z.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoid