Theorems · Definition · commutative algebra

RingCon.comapQuotientEquivOfSurj

{M : Type u_1} →
  {N : Type u_2} →
    [inst : NonAssocSemiring M] →
      [inst_1 : NonAssocSemiring N] →
        (c : RingCon M) →
          (f : N →+* M) → Function.Surjective ⇑f → {d : RingCon N} → d = c.comap f → d.Quotient ≃+* c.Quotient

A surjective ring homomorphism f : M →+* N induces a ring equivalence d.Quotient ≃+* c.Quotient, whenever c : RingCon M and d : RingCon N are such that d = c.comap f.

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

3 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringNonAssocSemiring