Theorems · Definition · commutative algebra

RingHom.HasStableEqualizers

({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop

A property P of ring homomorphisms is said to have stable equalizers, if the equalizer of algebra maps between algebras with structure morphisms satisfying P, is preserved by arbitrary base change.

Defined in

Mathlib.RingTheory.Flat.Equalizer

Cited by

3 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Quot.sound