RingHom.finiteType_is_local

theorem RingHom.finiteType_is_local : RingHom.PropertyIsLocal @RingHom.FiniteType

The theorem `RingHom.finiteType_is_local` states that the property of a ring homomorphism being of 'FiniteType' is local. This means that for a given ring homomorphism from ring A to ring B, if every localization of ring A at a prime ideal has the ring homomorphism property of 'FiniteType', then the original ring homomorphism also has the 'FiniteType' property. In other words, if B is finitely generated as an A-algebra for all localizations of A at a prime ideal, then B is finitely generated as an A-algebra.

More concisely: If every localization of a ring homomorphism from ring A to ring B preserves finiteness of types, then the homomorphism itself has finite type.