The meta properties of finitely-presented ring homomorphisms.

The main result is RingHom.finitePresentation_isLocal.

theorem RingHom.finitePresentation_localizationPreserves : LocalizationPreserves @FinitePresentation

Being finitely-presented is preserved by localizations.

theorem RingHom.finitePresentation_stableUnderComposition : StableUnderComposition @FinitePresentation

Being finitely-presented is stable under composition.

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_aux {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A] [Algebra.FinitePresentation R A] (f : A →ₐ[R] S) (hf : Function.Surjective ⇑f) (t : Finset A) (ht : Ideal.span ↑t = ⊤) (H : ∀ (g : { x : A // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))) : Algebra.FinitePresentation R S

If S is an R-algebra with a surjection from a finitely-presented R-algebra A, such that localized at a spanning set { r } of elements of A, Sᵣ is finitely-presented, then S is finitely presented. This is almost finitePresentation_ofLocalizationSpanTarget. The difference is, that here the set t generates the unit ideal of A, while in the general version, it only generates a quotient of A.

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.

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.