localization_away_map_finite — Mathlib

English

Localization away map preserves finiteness for ring homomorphisms.

Русский

Локализация away сохраняет конечность для кольцевых гомоморфизмов.

LaTeX

$$$\\operatorname{localization\\_away\\_map\\_finite}$$$

Lean4

theorem localization_away_map_finite (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.Finite) : (IsLocalization.Away.map R' S' f r).Finite :=
  finite_localizationPreserves.away f r _ _ hf

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