Theorems · Theorem · commutative algebra

Ideal.comp_quotientMap_eq_of_comp_eq

∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] {R' : Type u_5} {S' : Type u_6} [inst_2 : Ring R']
  [inst_3 : Ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f)
  (I : Ideal S') [inst_4 : I.IsTwoSided],
  have leq := ⋯;
  (Ideal.quotientMap I g' ⋯).comp (Ideal.quotientMap (Ideal.comap g' I) f ⋯) =
    (Ideal.quotientMap I f' ⋯).comp (Ideal.quotientMap (Ideal.comap f' I) g leq)

Commutativity of a square is preserved when taking quotients by an ideal.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Operations

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingRingRingRingIdeal.IsTwoSided