Commit 2026-05-24 17:27 7ea6142b

feat(Algebra/Category/Ring): Under.pushout preserves finite limits for properties with stable equalizers (#39572) We introduce a predicate RingHom.HasStableEqualizers for properties of ring homomorphisms: This is satisfied for P if base change along arbitrary ring homomorphisms preserves the equalizer of any two algebra maps between algebras satisfying P. In a follow-up PR we will show that finite étale ring homomorphisms satisfy this predicate. We relate RingHom.HasStableEqualizers to preservation of finite limits in P.Under R for R : CommRingCat. From Pi1.