Stalks of a scheme étale over a field are fields

Kollár starts the induction on the dimension at dim X = 0, where I = 𝒪_X because I is assumed nonzero on every irreducible component, and "everything is resolved without blow-ups" ([Kol07, 70]). In this library a scheme of dimension ≤ 0 over k has a structure morphism smooth of relative dimension 0, i.e. étale (Mathlib's Etale.iff_smoothOfRelativeDimension_zero), and the local rings of a scheme étale and locally of finite type over a field are fields: the stalk map 𝒪_{Spec k, f x} → 𝒪_{X, x} is a formally unramified local homomorphism essentially of finite type, so it carries the maximal ideal of its source onto that of its target ([TSPA, Tag 00UW], Mathlib's Algebra.FormallyUnramified.map_maximalIdeal), and the source, the localization of the field k at its only prime, is k itself. No perfectness of k is used (the route through the regularity of the stalk and the dimension formula Scheme.ringKrullDim_stalk_add_trdeg_residueField_of_smoothOfRelativeDimension would need [PerfectField k]): the statement holds over every field. Used for the base case of the induction on the dimension (Hironaka/Resolution/Algebraic/Stage/DimZero.lean).

theorem AlgebraicGeometry.isField_stalk_of_smoothOfRelativeDimension_zero {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [SmoothOfRelativeDimension 0 f] (x : ↥X) : IsField ↑(X.presheaf.stalk x)

The stalks of a scheme étale (smooth of relative dimension 0) and locally of finite type over a field are fields ([TSPA, Tag 00UW]; the case dim X = 0 of [Kol07, 70]): the stalk map is a formally unramified local homomorphism essentially of finite type, so the maximal ideal of 𝒪_{X, x} is generated by that of the base stalk, which is the field k.