Theorems · Theorem · commutative algebra

IsFractionRing.lift_algebraMap

∀ {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] [inst_4 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) (x : A),
  (IsFractionRing.lift hg) ((algebraMap A K) x) = g x

Given a commutative ring A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, the field hom induced from K to L maps x to g x for all x : A.

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingFieldFieldAlgebraIsFractionRing