Theorems · Theorem · commutative algebra

RingCon.lift_surjective_iff

∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  {h : c ≤ RingCon.ker f}, Function.Surjective ⇑(c.lift f h) ↔ Function.Surjective ⇑f

Surjective ring homomorphisms constant on the equivalence classes of a ring congruence relation induce a surjective homomorphism on the quotient.

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring