The meta properties of finitely-presented ring homomorphisms.

The main result is RingHom.finitePresentation_isLocal.

theorem RingHom.finitePresentation_stableUnderComposition : StableUnderComposition @FinitePresentation

Being finitely-presented is stable under composition.

theorem RingHom.finitePresentation_respectsIso : RespectsIso @FinitePresentation

Being finitely-presented respects isomorphisms.

theorem RingHom.finitePresentation_isStableUnderBaseChange : IsStableUnderBaseChange @FinitePresentation

Being finitely-presented is stable under base change.

theorem RingHom.finitePresentation_localizationPreserves : LocalizationPreserves @FinitePresentation

Being finitely-presented is preserved by localizations.

theorem RingHom.finitePresentation_holdsForLocalizationAway : HoldsForLocalizationAway @FinitePresentation

If R is a ring, then Rᵣ is R-finitely-presented for any r : R.

theorem RingHom.finitePresentation_ofLocalizationSpanTarget : OfLocalizationSpanTarget @FinitePresentation

Finite-presentation can be checked on a standard covering of the target.

theorem RingHom.finitePresentation_isLocal : PropertyIsLocal @FinitePresentation

Being finitely-presented is a local property of rings.