English
Locally P is a local property if it is preserved under localization and stable under base change, etc.
Русский
Locally P является локальным свойством, если оно сохраняется при локализации и устойчиво к базовым изменениями.
LaTeX
$$$\operatorname{PropertyIsLocal}(\Locally P).$$$
Lean4
/-- If `P` is preserved by localizations and stable under composition with localization
away maps, then `Locally P` is a local property of ring homomorphisms. -/
theorem locally_propertyIsLocal (hPl : LocalizationAwayPreserves P)
(hPa : StableUnderCompositionWithLocalizationAway P) : PropertyIsLocal (Locally P)
where
localizationAwayPreserves := locally_localizationAwayPreserves hPl
StableUnderCompositionWithLocalizationAwayTarget :=
locally_StableUnderCompositionWithLocalizationAwayTarget hPl.respectsIso hPa.right
ofLocalizationSpan :=
(locally_ofLocalizationSpanTarget hPl.respectsIso).ofLocalizationSpan
(locally_StableUnderCompositionWithLocalizationAwaySource hPa.left)
ofLocalizationSpanTarget := locally_ofLocalizationSpanTarget hPl.respectsIso
