Theorems · Definition · commutative algebra

Ideal.ResidueField.lift

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (I : Ideal R) →
          [inst_2 : I.IsPrime] →
            (f : R →+* S) →
              I ≤ RingHom.ker f → I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S) → I.ResidueField →+* S

If f sends I to 0 and Iᶜ to units, then f lifts to κ(I).

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingIdeal.IsPrime