Quasi-finiteness of the local homomorphism at a pair of primes

For an R-algebra S and primes q of S and p = q ∩ R of R, the local homomorphism R_p → S_q is quasi-finite iff S_q is quasi-finite over R, that is, iff S is quasi-finite over R at q (Algebra.QuasiFiniteAt R q): R_p is quasi-finite over R, and quasi-finiteness is transitive (Mathlib's Algebra.QuasiFinite.trans) and descends along the second map of a tower (Mathlib's Algebra.QuasiFinite.of_restrictScalars). Stalk maps of morphisms of affine schemes are such local homomorphisms, so this is how quasi-finiteness at a point is read off from a stalk.

Main results

• Localization.quasiFinite_localRingHom_iff: the local homomorphism R_p → S_q is quasi-finite iff S is quasi-finite over R at q.

theorem Localization.quasiFinite_localRingHom_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] (h : p = Ideal.comap (algebraMap R S) q) : (localRingHom p q (algebraMap R S) h).QuasiFinite ↔ Algebra.QuasiFiniteAt R q

The local homomorphism R_p → S_q at primes q over p is quasi-finite iff S is quasi-finite over R at q.