Theorems · Definition · commutative algebra

IsFractionRing.lift

{A : Type u_4} →
  [inst : CommRing A] →
    {K : Type u_5} →
      [inst_1 : Field K] →
        {L : Type u_7} →
          [inst_2 : Field L] →
            [inst_3 : Algebra A K] → [IsFractionRing A K] → {g : A →+* L} → Function.Injective ⇑g → K →+* L

Given a commutative ring A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, we get a field hom sending z : K to g x * (g y)⁻¹, where (x, y) : A × (NonZeroDivisors A) are such that z = f x * (f y)⁻¹.

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

12 results in Mathlib

Foundations

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

Assumes

CommRingFieldFieldAlgebraIsFractionRing