Theorems · Definition · commutative algebra

IsLocalization.sec

{R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → S → R × ↥M

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.RingTheory.Localization.Defs

Cited by

18 results in Mathlib

Foundations

Depth 18 from the axioms · uses Classical.choice

Assumes

CommSemiringCommSemiringAlgebraIsLocalization