Functoriality of the residue field at a prime ideal

For ring maps f : R → S and g : S → T and primes P, Q, Q' of R, S, T lying over one another, the maps κ(P) → κ(Q) → κ(Q') of Mathlib's Ideal.ResidueField.map compose to the map κ(P) → κ(Q') induced by g ∘ f. Thus residue fields are preserved along a composite when they are preserved along each step, as for a tower of étale neighbourhoods that do not extend the residue field at a point.

Main results

• Ideal.ResidueField.map_comp_map: the residue field maps of f and g compose to that of g ∘ f.

theorem Ideal.ResidueField.map_comp_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] (P : Ideal R) (Q : Ideal S) (Q' : Ideal T) [P.IsPrime] [Q.IsPrime] [Q'.IsPrime] (f : R →+* S) (g : S →+* T) (hf : P = comap f Q) (hg : Q = comap g Q') : (map Q Q' g hg).comp (map P Q f hf) = map P Q' (g.comp f) ⋯

The residue field maps κ(P) → κ(Q) along f and κ(Q) → κ(Q') along g compose to the residue field map κ(P) → κ(Q') along g ∘ f.