Clauses (1)–(3) of Theorem 36 are local on the base

The three clauses of [Kol07, Theorem 36], a smooth end result, an isomorphism over the smooth locus, and a simple normal crossing preimage of the singular locus, are local on the base. This is not stated in the sources as such: Kollár's gluing of the local resolutions ([Kol07, Proposition 37], "Putting together the proof of (27) with (37)" at the statement of Theorem 36) uses it implicitly, and his only locality remark, "(34.1) is a local property" in the proof of Theorem 36, concerns the functoriality clause. For a blow-up sequence T on X and a family of open immersions e i : W i ⟶ X covering X:

• smooth_composite_of_forall_pullback: the end result of T is smooth over a base f : X ⟶ B as soon as every T.pullback (e i) has a smooth end result over e i ≫ f; the last stage of T is covered by the last stages of the T.pullback (e i) (the stage lifts at the last index are the base changes of the e i, isPullback_pullbackStageHom), and Smooth is Zariski-local at the source; smooth_composite_pullback_of_isOpenImmersion is the converse restriction.
• isIso_morphismRestrict_composite_of_forall_pullback: T.composite is an isomorphism over an open V of X as soon as every (T.pullback (e i)).composite is an isomorphism over (e i) ⁻¹ᵁ V; isomorphisms are Zariski-local at the target, and over the piece V ∩ range (e i) the restriction of T.composite is the base change of T.composite along (e i) ⁻¹ᵁ V → X, which is the restriction of the pulled-back composite (Mathlib's morphismRestrictRestrict and morphismRestrictOpensRange, the pasted square); isIso_morphismRestrict_pullback_of_isOpenImmersion is the converse restriction.
• exists_snc_support_composite_of_forall_pullback: the preimage of a set S of X under T.composite is the support of a simple normal crossing family on the last stage as soon as it is on every T.pullback (e i) (Hironaka.Snc.exists_snc_of_openCover on the cover of the last stage by the last stages of the pulled-back sequences, Noetherian by isNoetherian_stage); exists_snc_support_pullback_of_isOpenImmersion is the converse restriction (the family pulled back along the stage lift, isSnc_comap_of_smooth; coe_support_comap), and preimage_compl_smoothLocus_eq transports the singular locus along an open immersion.

Both uses are instances of the same statements: the finite affine cover of a member of the class (the descent of the resolution functor, Hironaka.Resolution.Algebraic.Kol07.Thm36.Theorem36Assembly), and the empty cover of the empty scheme (the clauses hold vacuously there). The HEq transports stage_pullbackStageIdx_last, heq_stageMap_pullbackStageIdx_last, smooth_comp_of_heq and isIso_morphismRestrict_of_heq pass between the stage indexed by the transport of the last index (where the stage squares live) and the composite.

theorem Hironaka.Resolution.smooth_comp_of_heq {A B W V : AlgebraicGeometry.Scheme} (e : A = B) {g : A ⟶ W} {g' : B ⟶ W} (hg : g ≍ g') (p : W ⟶ V) (h : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp g p)) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp g' p)

Transport of smoothness of a composite along a HEq of the first factor.

theorem Hironaka.Resolution.stage_pullbackStageIdx_last {X W : AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (ι : W ⟶ X) : (T.pullback ι).stage (T.pullbackStageIdx ι (Fin.last T.length)) = (T.pullback ι).last

The stage of T.pullback ι indexed by the transport of the last index (pullbackStageIdx_last) is its last stage.

theorem Hironaka.Resolution.heq_stageMap_pullbackStageIdx_last {X W : AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (ι : W ⟶ X) : (T.pullback ι).stageMap (T.pullbackStageIdx ι (Fin.last T.length)) ≍ (T.pullback ι).composite

The stage map of T.pullback ι at the transport of the last index is its composite.

theorem Hironaka.Resolution.smooth_composite_pullback_of_isOpenImmersion {X W B : AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (ι : W ⟶ X) [AlgebraicGeometry.IsOpenImmersion ι] (f : X ⟶ B) (h : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp T.composite f)) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (T.pullback ι).composite (CategoryTheory.CategoryStruct.comp ι f))

Smoothness of the end result restricts along an open immersion of the base: the last stage of T.pullback ι is an open subscheme of the last stage of T.

theorem Hironaka.Resolution.smooth_composite_of_forall_pullback {ι : Type u_1} {X B : AlgebraicGeometry.Scheme} {W : ι → AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (e : (i : ι) → W i ⟶ X) [∀ (i : ι), AlgebraicGeometry.IsOpenImmersion (e i)] (hcov : ∀ (x : ↥X), ∃ (i : ι) (w : ↥(W i)), (e i) w = x) (f : X ⟶ B) (h : ∀ (i : ι), AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (T.pullback (e i)).composite (CategoryTheory.CategoryStruct.comp (e i) f))) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp T.composite f)

Clause (1) of [Kol07, Theorem 36] is local on the base (not stated in the sources): for a family of open immersions e i : W i ⟶ X covering X, the end result of T is smooth over the base as soon as every T.pullback (e i) has a smooth end result over the base.

theorem Hironaka.Resolution.isIso_morphismRestrict_of_heq {A B W : AlgebraicGeometry.Scheme} (e : A = B) {g : A ⟶ W} {g' : B ⟶ W} (hg : g ≍ g') (V : W.Opens) (h : CategoryTheory.IsIso (g ∣_ V)) : CategoryTheory.IsIso (g' ∣_ V)

Transport of IsIso of a restriction along a HEq of the morphism.

theorem Hironaka.Resolution.isIso_morphismRestrict_composite_of_forall_pullback {ι : Type u} {X : AlgebraicGeometry.Scheme} {W : ι → AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (e : (i : ι) → W i ⟶ X) [∀ (i : ι), AlgebraicGeometry.IsOpenImmersion (e i)] (hcov : ∀ (x : ↥X), ∃ (i : ι) (w : ↥(W i)), (e i) w = x) (V : X.Opens) (h : ∀ (i : ι), CategoryTheory.IsIso ((T.pullback (e i)).composite ∣_ (TopologicalSpace.Opens.map (e i).base).obj V)) : CategoryTheory.IsIso (T.composite ∣_ V)

Clause (2) of [Kol07, Theorem 36] is local on the base (not stated in the sources): IsIso (T.composite ∣_ V) holds as soon as, for a family of open immersions e i : W i ⟶ X covering X, every (T.pullback (e i)).composite is an isomorphism over (e i) ⁻¹ᵁ V.

Clause (3) and the converse restrictions

theorem Hironaka.Resolution.coe_support_comap {X Y : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (h : Y ⟶ X) : ↑(E.comap h).support = ⇑h ⁻¹' ↑E.support

The support of a pulled-back divisor family is the preimage of the support (Scheme.IdealSheafData.support_comap componentwise).

theorem Hironaka.Resolution.exists_snc_support_of_heq {A B W : AlgebraicGeometry.Scheme} (e : A = B) {g : A ⟶ W} {g' : B ⟶ W} (hg : g ≍ g') (S : Set ↥W) (h : ∃ (F : A.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑g ⁻¹' S) : ∃ (F : B.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑g' ⁻¹' S

Transport of a simple-normal-crossing-support statement along a HEq of the morphism.

theorem Hironaka.Resolution.exists_snc_support_pullback_of_isOpenImmersion {k : Type u} [Field k] [CharZero k] {X W : AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (ι : W ⟶ X) [AlgebraicGeometry.IsOpenImmersion ι] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp T.composite f)] (S : Set ↥X) (h : ∃ (F : T.last.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑T.composite ⁻¹' S) : ∃ (F : (T.pullback ι).last.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑(T.pullback ι).composite ⁻¹' ⇑ι ⁻¹' S

The simple-normal-crossing-support conclusion restricts along an open immersion ι of the base when the end result is smooth over k: the family pulled back along the stage lift (isSnc_comap_of_smooth).

theorem Hironaka.Resolution.exists_snc_support_composite_of_forall_pullback {ι : Type u} {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] {W : ι → AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (e : (i : ι) → W i ⟶ X) [∀ (i : ι), AlgebraicGeometry.IsOpenImmersion (e i)] (hcov : ∀ (x : ↥X), ∃ (i : ι) (w : ↥(W i)), (e i) w = x) (S : Set ↥X) (h : ∀ (i : ι), ∃ (F : (T.pullback (e i)).last.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑(T.pullback (e i)).composite ⁻¹' ⇑(e i) ⁻¹' S) : ∃ (F : T.last.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑T.composite ⁻¹' S

Clause (3) of [Kol07, Theorem 36] is local on the base (not stated in the sources): for a family of open immersions e i : W i ⟶ X covering X, if every (T.pullback (e i)).composite ⁻¹' ((e i) ⁻¹' S) is the support of a simple normal crossing family, so is T.composite ⁻¹' S (Hironaka.Snc.exists_snc_of_openCover); the last stage of T is Noetherian because X is (isNoetherian_stage).

theorem Hironaka.Resolution.isIso_morphismRestrict_pullback_of_isOpenImmersion {X W : AlgebraicGeometry.Scheme} (T : X.BlowUpSequence) (ι : W ⟶ X) [AlgebraicGeometry.IsOpenImmersion ι] (V : X.Opens) (h : CategoryTheory.IsIso (T.composite ∣_ V)) : CategoryTheory.IsIso ((T.pullback ι).composite ∣_ (TopologicalSpace.Opens.map ι.base).obj V)

IsIso of the restriction over an open V restricts along an open immersion ι of the base: (T.pullback ι).composite is an isomorphism over ι ⁻¹ᵁ V (the converse of isIso_morphismRestrict_composite_of_forall_pullback, by the same identification).

theorem Hironaka.Resolution.preimage_compl_smoothLocus_eq {X W B : AlgebraicGeometry.Scheme} (ι : W ⟶ X) [AlgebraicGeometry.IsOpenImmersion ι] (f : X ⟶ B) [AlgebraicGeometry.LocallyOfFinitePresentation f] : ⇑ι ⁻¹' (↑(AlgebraicGeometry.Scheme.Hom.smoothLocus f))ᶜ = (↑(AlgebraicGeometry.Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp ι f)))ᶜ

The preimage of the singular locus along an open immersion ι is the singular locus of the composite structure morphism, as sets (Scheme.Hom.preimage_smoothLocus_eq).