Closed points of the blow-up are rational over their image

[Hau14, Proposition 5.4] and [Hau03, Appendix C] work with closed points of varieties over an algebraically closed field K, where the entries a'_i ∈ K of a point a' of the blow-up make sense. The statements (8)–(9) of that proposition in Hironaka.Scheme.Snc.ChartOrigin carry the hypothesis that a' is rational over κ(a), a = π(a'): the residue field map κ(a) → κ(a') is an isomorphism. This module discharges it in Hauser's setting: for X smooth over an algebraically closed k and a' a closed point of B_Z X, both residue fields are k (Mathlib's residueFieldIsoBase, for the closed points a' and a = π(a') — the image of a closed point under the proper blow-up map is closed), and the residue field map is the composite of these identifications (isIso_residueFieldMap_of_isClosed), by the naturality Spec.map (π^♯) ≫ fromSpecResidueField = fromSpecResidueField ≫ π and the faithfulness of Spec.

theorem AlgebraicGeometry.isIso_residueFieldMap_of_isClosed {k : Type u} [Field k] {X : Scheme} [IsAlgClosed k] (f : X ⟶ Spec ↧k) [Smooth f] (Z : X.IdealSheafData) (a' : ↥Z.blowUp) (hcl : IsClosed {a'}) : CategoryTheory.IsIso (Scheme.Hom.residueFieldMap Z.blowUpπ a')

Hauser's setting for (6), (8), (9): for k algebraically closed and a' a closed point of B_Z X, the residue field map κ(π a') → κ(a') of the blow-up is an isomorphism (both fields are k).