English
Being finitely presented is a local property of rings: it can be checked on a suitable covering by localizations.
Русский
Свойство конечного презентирования является локальным свойством колец: его можно проверить на подходящем покрытии локализациями.
LaTeX
$$$\text{PropertyIsLocal }\operatorname{FinitePresentation}$$$
Lean4
/-- Being finitely-presented is a local property of rings. -/
theorem finitePresentation_isLocal : PropertyIsLocal @FinitePresentation :=
⟨finitePresentation_localizationPreserves.away, finitePresentation_ofLocalizationSpanTarget,
finitePresentation_ofLocalizationSpanTarget.ofLocalizationSpan
(finitePresentation_stableUnderComposition.stableUnderCompositionWithLocalizationAway
finitePresentation_holdsForLocalizationAway).left,
(finitePresentation_stableUnderComposition.stableUnderCompositionWithLocalizationAway
finitePresentation_holdsForLocalizationAway).right⟩
