Commit 2024-10-16 05:50 7a8cf3c4

feat(AlgebraicGeometry/RingHomProperties): a property induced from Locally Q is equivalent to locally Q (#17305) If P is a morphism property of schemes associated to the property Locally Q for a property of ring homomorphisms Q, then for a morphism f, P f is equivalent to: for every point x in the source there exist open affine neighborhoods around x and f.val.base x respectively such that the induced map of rings satisfies Q. This guarantees that we may define properties of scheme morphisms explicitly as described above for properties of ring homomorphisms that are not necessarily local at the target and still use the API for HasRingHomProperty.