Theorems · Definition · commutative algebra

Ideal.quotientMap

{R : Type u} →
  [inst : Ring R] →
    {S : Type v} →
      [inst_1 : Ring S] →
        {I : Ideal R} →
          (J : Ideal S) →
            [inst_2 : I.IsTwoSided] → [inst_3 : J.IsTwoSided] → (f : R →+* S) → I ≤ Ideal.comap f J → R ⧸ I →+* S ⧸ J

The ring hom R/I →+* S/J induced by a ring hom f : R →+* S with I ≤ f⁻¹(J)

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

27 results in Mathlib

Foundations

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

Assumes

RingRingIdeal.IsTwoSidedIdeal.IsTwoSided