locallyOfFinitePresentation_of_isOpenImmersion

English

If f is locally of finite presentation, then localization behaves well under base change and pullbacks.

Русский

Если f локально презентационен, топологически локальные свойства сохраняются под базовым изменением и вытяжением.

LaTeX

$$$[\text{LocallyOfFinitePresentation}(f)] \Rightarrow \text{preserves localization and base change}.$$$

Lean4

instance (priority := 900) locallyOfFinitePresentation_of_isOpenImmersion [IsOpenImmersion f] :
    LocallyOfFinitePresentation f :=
  HasRingHomProperty.of_isOpenImmersion RingHom.finitePresentation_holdsForLocalizationAway.containsIdentities

Похожие утверждения