Artinian fibres and residue fields of quasi-finite algebras

For a prime q at which S is quasi-finite over R, the local-ring localization equivalence identifies the fibre S_q ⧸ (q.under R) S_q with an Artinian quotient of the localization of S_q at its maximal ideal.

For a quasi-finite local homomorphism R → S of local rings, the residue field of S is a finite extension of the residue field of R.

Main results

• Ideal.isArtinianRing_quotient_of_quasiFiniteAt: the local fibre at a quasi-finite prime is Artinian.
• IsLocalRing.ResidueField.finite_of_quasiFinite: the residue field extension of a quasi-finite local homomorphism of local rings is finite.

References

• The Stacks Project, Tag 00PK (a quasi-finite ring map has finite residue field extensions).

instance Ideal.isArtinianRing_quotient_of_quasiFiniteAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) [q.IsPrime] [Algebra.QuasiFiniteAt R q] : IsArtinianRing (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))

If S is quasi-finite over R at a prime q, the quotient of S_q by the extension of q.under R is an Artinian ring.

instance IsLocalRing.ResidueField.finite_of_quasiFinite {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Algebra.QuasiFinite R S] : Module.Finite (ResidueField R) (ResidueField S)

The residue field extension of a quasi-finite local homomorphism is finite. If R → S is a local homomorphism of local rings and S is quasi-finite over R, then the residue field of S is a finite extension of the residue field of R. Stacks, Lemma 00PK. The proof follows that of Mathlib's instance Module.Finite P.ResidueField Q.ResidueField for primes of a quasi-finite algebra in Mathlib/RingTheory/QuasiFinite/Basic.lean.