Theorems · Definition · commutative algebra

Ideal.Quotient.algebraQuotientOfLEComap

{A : Type u_3} →
  [inst : Ring A] →
    {R : Type u_5} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R A] →
          {p : Ideal R} →
            {P : Ideal A} → [inst_3 : P.IsTwoSided] → p ≤ Ideal.comap (algebraMap R A) P → Algebra (R ⧸ p) (A ⧸ P)

If P lies over p, then R / p has a canonical map to A / P.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

4 results in Mathlib

Foundations

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

Assumes

RingCommRingAlgebraIdeal.IsTwoSided