A blow-up sequence is an isomorphism over the locus its centers avoid

Clause (3) of [Kol07, Theorem 35] says the principalization Π : X_r → X is an isomorphism over X ∖ cosupp I; the reason is the general fact that a composite of blow-ups whose centers lie over a closed set Z is an isomorphism over X ∖ Z: a blow-up is an isomorphism off its center (blowUp.isIso_π_restrict_compl_support, [TSPA, Tag 02OS]) and the restriction of a composite to an open is the composite of the restrictions (morphismRestrict_comp). This module proves that statement for sequences, isIso_composite_restrict_of_centers_disjoint, by induction along the sequence, from two general tools:

• isIso_restrict_of_le: an isomorphism over an open V is an isomorphism over every open U ≤ V, because f ∣_ U is the base change of f ∣_ V along U ⟶ V (the two squares of isPullback_morphismRestrict, pasted by IsPullback.of_bot) and isomorphisms are stable under base change;
• isIso_eraseEmpty_composite_restrict: deleting the empty blow-ups does not change the isomorphism locus, because the composite of S.eraseEmpty is the composite of S after the isomorphism eraseEmptyLastHom of the last stages (eraseEmptyLastHom_comp_composite).

The stalkwise form of the same fact is isIso_over_of_centers_disjoint of Hironaka/Resolution/Algebraic/Kol07/IsoLocus.lean; here the conclusion is the isomorphism of the restriction S.composite ∣_ U itself, the form in which clause (3) of the principalization theorem is stated. Holds on any scheme.

theorem Hironaka.Sequence.isIso_restrict_congr {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y} (e : f = g) (U : Y.Opens) [CategoryTheory.IsIso (f ∣_ U)] : CategoryTheory.IsIso (g ∣_ U)

IsIso of a restriction is transported along an equality of morphisms (the two restrictions have different source objects only up to that equality, so rw cannot do it in place).

theorem Hironaka.Sequence.isIso_restrict_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) [CategoryTheory.IsIso (f ∣_ (TopologicalSpace.Opens.map g.base).obj U)] [CategoryTheory.IsIso (g ∣_ U)] : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g ∣_ U)

The restriction of a composite is an isomorphism when both restricted factors are (morphismRestrict_comp; the source objects (f ≫ g) ⁻¹ᵁ U and f ⁻¹ᵁ (g ⁻¹ᵁ U) agree only by unfolding, hence the explicit inferInstanceAs).

theorem Hironaka.Sequence.isIso_restrict_of_le {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U V : Y.Opens} (h : U ≤ V) [CategoryTheory.IsIso (f ∣_ V)] : CategoryTheory.IsIso (f ∣_ U)

An isomorphism over an open V is an isomorphism over every open U ≤ V: the restriction f ∣_ U is the base change of f ∣_ V along U ⟶ V (the two squares of isPullback_morphismRestrict, pasted vertically), and isomorphisms are stable under base change.

theorem Hironaka.Sequence.isIso_composite_restrict_of_centers_disjoint {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (U : X.Opens) : (∀ (i : Fin S.length), Disjoint (↑(S.center i).support) (⇑(S.stageMap i.castSucc) ⁻¹' ↑U)) → CategoryTheory.IsIso (S.composite ∣_ U)

A blow-up sequence whose centers avoid the preimages of an open U is an isomorphism over U (the general form of clause (3) of [Kol07, Theorem 35]): by induction along the sequence, each blow-up being an isomorphism off its center (blowUp.isIso_π_restrict_compl_support, [TSPA, Tag 02OS], restricted to U by isIso_restrict_of_le) and the restriction of a composite being the composite of the restrictions (morphismRestrict_comp).

theorem Hironaka.Sequence.isIso_eraseEmpty_composite_restrict {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (U : X.Opens) [CategoryTheory.IsIso (S.composite ∣_ U)] : CategoryTheory.IsIso (S.eraseEmpty.composite ∣_ U)

Deleting the empty blow-ups does not change the isomorphism locus: the composite of S.eraseEmpty is the composite of S after the isomorphism eraseEmptyLastHom of the last stages.