Resolution of a variety by a single blow-up, in Mathlib's terms

Hironaka's Main Theorem I [Hir64, p. 132] (AlgebraicGeometry.exists_isBlowUpAlong_smooth): an integral scheme X, separated and of finite type over a field k of characteristic zero, has a blow-up π : X' → X along an ideal sheaf supported exactly on the singular locus, with X' smooth over k; π is proper and an isomorphism over the smooth locus of X. It is stated with Mathlib's definitions and two that Mathlib lacks, effective Cartier ideal sheaves and blow-ups given by their universal property, defined from Mathlib's alone (Scheme.IdealSheafData.IsEffectiveCartier, Scheme.Hom.IsBlowUpAlong, in Hironaka.Scheme.BlowUp.BlowUpAlong.Defs, a module importing Mathlib only), so that the challenge file Challenge/Standard.lean imports Mathlib only and repeats the two definitions word for word. They are the library's Scheme.IdealSheafData.IsInvertible and IsBlowUp (Scheme.Hom.isBlowUpAlong_iff_isBlowUp).

It is the library's Main Theorem I, AlgebraicGeometry.exists_support_eq_singularLocus_isRegular_blowUp, for X with its structure morphism as an algebraic k-scheme, read in Mathlib's terms: the resolution is the blow-up D.blowUp → X along an ideal sheaf D supported on the singular locus, which has the universal property of the blow-up (Scheme.IdealSheafData.blowUp.isBlowUp, read through Scheme.Hom.isBlowUpAlong_iff_isBlowUp). It is proper because X is locally Noetherian (Scheme.IdealSheafData.blowUp.isProper_π) and an isomorphism over the complement of the support of D (Scheme.IdealSheafData.blowUp.isIso_π_restrict_compl_support), which is the smooth locus of X since over the perfect field k the singular locus is the complement of the smooth locus (Scheme.singularLocus_eq_compl_smoothLocus, [TSPA, Tag 00TV]); and D.blowUp is regular, hence smooth over k (Scheme.smooth_iff_isRegular).

theorem AlgebraicGeometry.exists_isBlowUpAlong_smooth {k : Type u} [Field k] [CharZero k] (X : Scheme) (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] [IsIntegral X] : ∃ (X' : Scheme) (π : X' ⟶ X) (I : X.IdealSheafData), Scheme.Hom.IsBlowUpAlong π I ∧ ↑I.support = (↑(Scheme.Hom.smoothLocus f))ᶜ ∧ Smooth (CategoryTheory.CategoryStruct.comp π f) ∧ IsProper π ∧ CategoryTheory.IsIso (π ∣_ Scheme.Hom.smoothLocus f)

Resolution of singularities [Hir64, Main Theorem I, p. 132]. Every integral scheme X, separated and of finite type over a field k of characteristic zero, is resolved by a single blow-up: there is a blow-up π : X' → X along an ideal sheaf supported exactly on the singular locus of X, with X' smooth over k. In particular π is proper and an isomorphism over the smooth locus.

Relation to the source.

• Translation. Hironaka's "non-singular" (every local ring regular) is read as smooth over k, Smooth (π ≫ f), and his singular locus as the complement of the smooth locus f.smoothLocus: for schemes locally of finite type over a field of characteristic zero the two notions agree [TSPA, Tag 00TV].
• Interpretation. Hironaka's "say reduced and irreducible" is read as the hypothesis IsIntegral X.

Source statement: [Hir64, Main Theorem I, p. 132]