English
A property P of ring homomorphisms is said to be stable under composition with localization away on both the source and the target if P(f) implies P when composed with left and right localization maps.
Русский
Свойство P гомоморфизмов колец стабильно при композиции с локализацией слева и справа на источнике и целевой стороне, если из P(f) следует сохранение свойства после таких локализаций.
LaTeX
$$$\mathrm{StableUnderCompositionWithLocalizationAway}(P) = \big(\mathrm{StableUnderCompositionWithLocalizationAwaySource}P\big) \wedge \big(\mathrm{StableUnderCompositionWithLocalizationAwayTarget}P\big)$$$
Lean4
/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAway`
if whenever `P` holds for `f` it also holds for the composition with
localization maps on the left and on the right. -/
def StableUnderCompositionWithLocalizationAway : Prop :=
StableUnderCompositionWithLocalizationAwaySource P ∧ StableUnderCompositionWithLocalizationAwayTarget P
