localization_away_map_finiteType — Mathlib

English

The map induced by localization Away preserves finite type: if f is FP, then its localization map is FP.

Русский

Карта локализации Away сохраняет FP: если отображение FP, то и локализованная карта FP.

LaTeX

$$$\text{Away.map FP}$$$

Lean4

theorem localization_away_map_finiteType (R S R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
    [Algebra R R'] (f : R →+* S) [Algebra S S'] (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S']
    (hf : f.FiniteType) : (IsLocalization.Away.map R' S' f r).FiniteType :=
  finiteType_localizationPreserves.away _ r _ _ hf

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