Theorems · Definition · commutative algebra

RingCon.lift

{M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring P] → (c : RingCon M) → (f : M →+* P) → c ≤ RingCon.ker f → c.Quotient →+* P

The homomorphism on the quotient of a ring by a congruence relation c induced by a homomorphism constant on the equivalence classes of c.

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

16 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

NonAssocSemiringNonAssocSemiring