The meta properties of finite-type ring homomorphisms.

Main results

Let R be a commutative ring, S is an R-algebra, M be a submonoid of R.

• finiteType_localizationPreserves : If S is a finite type R-algebra, then S' = M⁻¹S is a finite type R' = M⁻¹R-algebra.
• finiteType_ofLocalizationSpan : S is a finite type R-algebra if there exists a set { r } that spans R such that Sᵣ is a finite type Rᵣ-algebra.
• RingHom.finiteType_isLocal: RingHom.FiniteType is a local property.

theorem RingHom.finiteType_stableUnderComposition : StableUnderComposition @FiniteType

theorem RingHom.finiteType_respectsIso : RespectsIso @FiniteType

theorem RingHom.finiteType_isStableUnderBaseChange : IsStableUnderBaseChange @FiniteType

theorem RingHom.finiteType_localizationPreserves : LocalizationPreserves @FiniteType

If S is a finite type R-algebra, then S' = M⁻¹S is a finite type R' = M⁻¹R-algebra.

theorem RingHom.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

theorem RingHom.finiteType_ofLocalizationSpan : OfLocalizationSpan @FiniteType

theorem RingHom.finiteType_holdsForLocalizationAway : HoldsForLocalizationAway @FiniteType

theorem RingHom.finiteType_ofLocalizationSpanTarget : OfLocalizationSpanTarget @FiniteType

theorem RingHom.finiteType_isLocal : PropertyIsLocal @FiniteType