Base-change properties of induced quotient maps

For a ring homomorphism f : A →+* B, the induced map A/I → B/IB is a base change of f. Hence it inherits every ring-homomorphism property stable under base change and isomorphism. This applies, in particular, to faithful flatness and finite presentation.

theorem RingHom.IsStableUnderBaseChange.quotientMap {P : {A B : Type u} → [inst : CommRing A] → [inst_1 : CommRing B] → (A →+* B) → Prop} (hP : IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) (hiso : RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) {A B : Type u} [CommRing A] [CommRing B] (f : A →+* B) (I : Ideal A) (hf : P f) : P (Ideal.quotientMap (Ideal.map f I) f ⋯)

A property stable under base change and isomorphism passes from f : A →+* B to A/I → B/IB.