mathlib

912a310a - refactor(category_theory/morphism_property): stable_under_base_change (#16196)

refactor(category_theory/morphism_property): stable_under_base_change (#16196) This PR redefines `morphism_property.stable_under_base_change P`. This condition now states that for all pullback squares (`is_pullback`), the left map satisfies the property if the right map does. Then, it is automatic that the property `P` respects isos. A constructor is provided to take as an input the assumption that `P` respects isos and the previous condition that if a map `g` satisfies `P`, then `pullback.fst : pullback f g → _` satisfies it `P`.