Theorems · Theorem · commutative algebra

RingCon.mapGen_eq_map_of_surjective

∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M} (f : M →+* N),
  RingCon.ker f ≤ c → Function.Surjective ⇑f → ⇑(RingCon.mapGen ⇑f) = Relation.Map ⇑c ⇑f ⇑f

If c is a ring congruence on M, then the smallest ring congruence relation on N deduced from c by a ring homomorphism from M to N is the relation deduced from c.

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring