Commit 2024-09-19 10:59 53bac4a8

chore(AlgebraicGeometry): weaken assumptions on local ring hom properties (#16897) Currently for a property of ring homomorphisms P, the predicate RingHom.PropertyIsLocal P requires P to be stable under composition. This predicate is meant to capture the requirements to guarantee that affineLocally P is local on the source and on the target. But for the latter it is sufficient to ask that P is stable under composition with localization maps away from one element. Hence we replace StableUnderComposition P and HoldsForLocalizationAway P with StableUnderCompositionWithLocalizationAway P. Before this change, every P satisfying RingHom.PropertyIsLocal was satisfied by all identities and localization maps away from one element. In particular affineLocally P was satisfied by all open immersions. Now this is no longer automatic, since P does not necessarily contain identities. This change is necessary to apply the HasRingHomProperty API to the class of ring homomorphisms that are standard smooth of a fixed relative dimension n > 0, since these are not stable under composition (the compositions add up), but are stable under composition with localization maps. This change turns some instances into theorems and hence slightly reduces automation. The fallout is relatively small.