Transport of the end-result clauses along an isomorphism of last stages

Clauses (1)–(3) of [Kol07, Theorem 36] speak about the end result X_r of a blow-up sequence and its composite Π : X_r → X: the end result is smooth, Π is an isomorphism over the smooth locus, Π⁻¹(Sing X) is the support of a simple normal crossing family. The resolution functor deletes the empty blow-ups of the affine resolution ([Kol07, 32] and the second bullet of [Kol07, 34.1]), a harmless change of the sequence that leaves the composite unchanged up to an isomorphism of the last stages. This module records the isomorphism and the transport of the three clauses:

• eraseEmptyLastIso S : S.eraseEmpty.last ≅ S.last with (eraseEmptyLastIso S).hom ≫ S.composite = S.eraseEmpty.composite (from eraseEmptyLastHom of Hironaka/Scheme/BlowUpSequence/EraseEmptyConcat.lean, an isomorphism by isIso_eraseEmptyLastHom);
• for an isomorphism e : S'.last ≅ S.last with e.hom ≫ S.composite = S'.composite: smooth_composite_of_lastIso, isIso_composite_restrict_of_lastIso, exists_isSnc_support_eq_preimage_of_lastIso: clauses (1), (2), (3) pass from S to S' (the simple normal crossing family is pulled back along the isomorphism, isSnc_comap_of_smooth);
• the same three clauses pass between two sequences with the same erasure.

The isomorphism of last stages

noncomputable def Hironaka.Sequence.eraseEmptyLastIso {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : S.eraseEmpty.last ≅ S.last

The last stage of the sequence with its empty blow-ups deleted is isomorphic to the last stage of the sequence (eraseEmptyLastHom is an isomorphism).

Equations

• Hironaka.Sequence.eraseEmptyLastIso S = CategoryTheory.asIso S.eraseEmptyLastHom

theorem Hironaka.Sequence.eraseEmptyLastIso_hom_comp_composite {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : CategoryTheory.CategoryStruct.comp (eraseEmptyLastIso S).hom S.composite = S.eraseEmpty.composite

Transport of the three clauses

theorem Hironaka.Sequence.smooth_composite_of_lastIso {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S'.last ≅ S.last) (he : CategoryTheory.CategoryStruct.comp e.hom S.composite = S'.composite) {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp S.composite f)] : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp S'.composite f)

Clause (1) along an isomorphism of last stages: the end result stays smooth.

theorem Hironaka.Sequence.isIso_composite_restrict_of_lastIso {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S'.last ≅ S.last) (he : CategoryTheory.CategoryStruct.comp e.hom S.composite = S'.composite) (W : X.Opens) [CategoryTheory.IsIso (S.composite ∣_ W)] : CategoryTheory.IsIso (S'.composite ∣_ W)

Clause (2) along an isomorphism of last stages: the composite stays an isomorphism over an open W of the base.

theorem Hironaka.Sequence.exists_isSnc_support_eq_preimage_of_lastIso {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S'.last ≅ S.last) (he : CategoryTheory.CategoryStruct.comp e.hom S.composite = S'.composite) {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp S.composite f)] (W : Set ↥X) (h : ∃ (F : S.last.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑S.composite ⁻¹' W) : ∃ (F' : S'.last.DivisorFamily), F'.IsSnc ∧ ↑F'.support = ⇑S'.composite ⁻¹' W

Clause (3) along an isomorphism of last stages: an snc family whose support is the preimage of a set W of the base pulls back to one on the other last stage (isSnc_comap_of_smooth along the isomorphism, which is smooth; the end result is smooth over k by clause (1)).

Two sequences with the same erasure

theorem Hironaka.Sequence.smooth_composite_of_eraseEmpty_eq {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (h : S.eraseEmpty = S'.eraseEmpty) {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp S.composite f)] : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp S'.composite f)

Clause (1) passes between two sequences with the same erasure.

theorem Hironaka.Sequence.isIso_composite_restrict_of_eraseEmpty_eq {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (h : S.eraseEmpty = S'.eraseEmpty) (W : X.Opens) [CategoryTheory.IsIso (S.composite ∣_ W)] : CategoryTheory.IsIso (S'.composite ∣_ W)

Clause (2) passes between two sequences with the same erasure.

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

Clause (3) passes between two sequences with the same erasure.