The first-centre index along pushforwards and isomorphisms

Kollár reduces the independence of the resolution of an affine scheme from its embedding to embeddings into affine spaces, using that the principalization functor commutes with closed embeddings and with isomorphisms [Kol07, Theorem 36, proof; Theorem 35 (4), (5)]. This file proves the bookkeeping behind that reduction: the index firstCenterIndex is invariant under the pushforward of a blow-up sequence along a closed immersion and under the pullback along an isomorphism, because the predicate CenterContains transports exactly.

• Along a closed immersion j : Y ⟶ X, the centres of S.pushforward j are the images of the centres, and the strict transform of I.map j along the pushforward is the image of the strict transform of I along S (strictTransformSeq_pushforward; one step is strictTransform_map, which identifies the strict transform of the image of a closed immersion with the kernel of the lift of that immersion to the blow-up). Taking images along a closed immersion is an order embedding, so CenterContains and the index transport (firstCenterIndex_pushforward).
• Along an isomorphism φ, the centres and strict transforms of S.pullback φ are the inverse images of those of S, again an order embedding (firstCenterIndex_pullback_of_isIso).
• BR_affine_comp_eq_of_BP_eq_pushforward and BR_affine_eq_of_BP_eq_pullback: BR_affine is unchanged along a closed embedding, respectively an isomorphism, of the ambient triples, granted the corresponding identity for BP (which Hironaka.Resolution.Algebraic.Kol07.Thm36.Assembly supplies from the functoriality of the principalization sequence).

The strict transform of a pushed-forward ideal

theorem Hironaka.Resolution.strictTransform_ker {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion f] (D : X.IdealSheafData) : (AlgebraicGeometry.Scheme.Hom.ker f).strictTransform D = AlgebraicGeometry.Scheme.Hom.ker (AlgebraicGeometry.Scheme.Hom.blowUpMap f D)

The strict transform under the blow-up of D of the kernel of a closed immersion f is the kernel of the lift blowUpMap f D of f to the blow-ups.

theorem Hironaka.Resolution.comap_map_comp {X Y W : AlgebraicGeometry.Scheme} (ι : W ⟶ Y) (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (Z : Y.IdealSheafData) : (Z.map j).comap (CategoryTheory.CategoryStruct.comp ι j) = Z.comap ι

The inverse image of Z.map j under ι ≫ j, for a closed immersion j, is the inverse image of Z under ι.

theorem Hironaka.Resolution.blowUpMap_comp_pushforwardBlowUp {X Y W : AlgebraicGeometry.Scheme} (ι : W ⟶ Y) (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (Z : Y.IdealSheafData) : AlgebraicGeometry.Scheme.Hom.blowUpMap (CategoryTheory.CategoryStruct.comp ι j) (Z.map j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.blowUpMap ι Z) (AlgebraicGeometry.Scheme.Hom.pushforwardBlowUp j Z))

The lift of a composite ι ≫ j, with j a closed immersion, to the blow-up of the image Z.map j is the lift of ι to the blow-up of Z followed by the inclusion of blow-ups pushforwardBlowUp j Z, up to the identification of the sources [Kol07, Definition 30, 30.3].

theorem Hironaka.Resolution.strictTransform_map {X Y : AlgebraicGeometry.Scheme} (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (Z I : Y.IdealSheafData) : (I.map j).strictTransform (Z.map j) = (I.strictTransform Z).map (AlgebraicGeometry.Scheme.Hom.pushforwardBlowUp j Z)

One step of [Kol07, Definition 30, 30.2–30.3]: the strict transform of the image I.map j under the blow-up of the image centre Z.map j, for a closed immersion j, is the image, along the inclusion pushforwardBlowUp j Z of the blow-ups, of the strict transform of I under the blow-up of Z.

theorem Hironaka.Resolution.strictTransformSeq_pushforward_mk {X Y : AlgebraicGeometry.Scheme} (S : Y.BlowUpSequence) (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (I : Y.IdealSheafData) (n : ℕ) (hn : n < S.length + 1) : (S.pushforward j).strictTransformSeq (I.map j) (S.pushforwardStageIdx j ⟨n, hn⟩) = (S.strictTransformSeq I ⟨n, hn⟩).map (S.pushforwardStageHom j ⟨n, hn⟩)

Along the pushforward of a sequence S along a closed immersion j, the strict transform of I.map j is the image, along the stage inclusion, of the strict transform of I along S [Kol07, Definition 30, 30.2–30.3]; the indices are given as ⟨n, hn⟩. By induction on the sequence, with strictTransform_map at the head.

theorem Hironaka.Resolution.strictTransformSeq_pushforward {X Y : AlgebraicGeometry.Scheme} (S : Y.BlowUpSequence) (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (I : Y.IdealSheafData) (i : Fin (S.length + 1)) : (S.pushforward j).strictTransformSeq (I.map j) (S.pushforwardStageIdx j i) = (S.strictTransformSeq I i).map (S.pushforwardStageHom j i)

The strict transform of a pushed-forward ideal sheaf along the pushed-forward sequence is the image of the strict transform along the stage inclusion [Kol07, Definition 30, 30.2–30.3].

Order embeddings

theorem Hironaka.Resolution.map_le_map_iff_of_isClosedImmersion {X Y : AlgebraicGeometry.Scheme} (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] {A B : Y.IdealSheafData} : A.map j ≤ B.map j ↔ A ≤ B

map along a closed immersion reflects and preserves inclusions (comap_map_of_isClosedImmersion).

theorem Hironaka.Resolution.comap_le_comap_iff_of_isIso {X Y : AlgebraicGeometry.Scheme} (φ : Y ⟶ X) [CategoryTheory.IsIso φ] {A B : X.IdealSheafData} : A.comap φ ≤ B.comap φ ↔ A ≤ B

comap along an isomorphism reflects and preserves inclusions.

The first-centre index along a pushforward

theorem Hironaka.Resolution.centerContains_pushforward_iff {X Y : AlgebraicGeometry.Scheme} (S : Y.BlowUpSequence) (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (I : Y.IdealSheafData) (n : ℕ) : CenterContains (S.pushforward j) (I.map j) n ↔ CenterContains S I n

The predicate "the n-th centre contains the strict transform" transports exactly along the pushforward of a sequence along a closed immersion: the centres and strict transforms of the pushforward are the images of those of S, and taking images is an order embedding.

theorem Hironaka.Resolution.firstCenterIndex_pushforward {X Y : AlgebraicGeometry.Scheme} (S : Y.BlowUpSequence) (j : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion j] (I : Y.IdealSheafData) : firstCenterIndex (S.pushforward j) (I.map j) = firstCenterIndex S I

The first-centre index of the pushed-forward sequence for the pushed-forward ideal sheaf is the first-centre index of the original.

The first-centre index along an isomorphism

theorem Hironaka.Resolution.isIso_pullbackStageHom_mk {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (φ : Y ⟶ X) [CategoryTheory.IsIso φ] (n : ℕ) (hn : n < S.length + 1) : CategoryTheory.IsIso (S.pullbackStageHom φ ⟨n, hn⟩)

The stage lifts of the pullback of a sequence along an isomorphism are isomorphisms (each is the lift of an isomorphism to the blow-ups, isIso_blowUpMap_of_isIso).

theorem Hironaka.Resolution.centerContains_pullback_iff_of_isIso {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (φ : Y ⟶ X) [CategoryTheory.IsIso φ] (I : X.IdealSheafData) (n : ℕ) : CenterContains (S.pullback φ) (I.comap φ) n ↔ CenterContains S I n

The predicate "the n-th centre contains the strict transform" transports exactly along the pullback of a sequence along an isomorphism φ: centres and strict transforms of the pullback are the inverse images of those of S, and inverse image along φ is an order embedding.

theorem Hironaka.Resolution.firstCenterIndex_pullback_of_isIso {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (φ : Y ⟶ X) [CategoryTheory.IsIso φ] (I : X.IdealSheafData) : firstCenterIndex (S.pullback φ) (I.comap φ) = firstCenterIndex S I

The first-centre index of the pullback of a sequence along an isomorphism, for the pulled-back ideal sheaf, is the first-centre index of the original (the case of an automorphism of the ambient space in the proof of [Kol07, Theorem 36]).

BR_affine along a closed embedding and along an isomorphism of the ambient triples

theorem Hironaka.Resolution.BR_affine_comp_eq_of_BP_eq_pushforward {k : Type u} [Field k] [CharZero k] (TA TA' : AlgebraicGeometry.Triple k) (j : TA.X.left ⟶ TA'.X.left) [AlgebraicGeometry.IsClosedImmersion j] (hBP : Sequence.BP TA' = (Sequence.BP TA).pushforward j) (hI : TA'.I = TA.I.map j) {X : AlgebraicGeometry.Scheme} (emb : X ⟶ TA.X.left) : BR_affine TA' (CategoryTheory.CategoryStruct.comp emb j) = BR_affine TA emb

BR_affine is unchanged along a closed embedding of the ambient triples, granted that the principalization sequences correspond: if BP TA' = (BP TA).pushforward j for a closed immersion j of the ambients and TA'.I = TA.I.map j, then BR_affine built through TA' from the embedding emb ≫ j equals BR_affine built in TA from emb. The first-centre index is the same (firstCenterIndex_pushforward), truncation commutes with the pushforward, and restricting a pushed-forward sequence to X gives back the restriction of the original. The hypothesis is [Kol07, Theorem 35 (5)], supplied in Hironaka.Resolution.Algebraic.Kol07.Thm36.Assembly.

theorem Hironaka.Resolution.BR_affine_eq_of_BP_eq_pullback {k : Type u} [Field k] [CharZero k] (TA TA' : AlgebraicGeometry.Triple k) (φ : TA'.X.left ⟶ TA.X.left) [CategoryTheory.IsIso φ] (hBP : Sequence.BP TA' = (Sequence.BP TA).pullback φ) (hI : TA'.I = TA.I.comap φ) {X : AlgebraicGeometry.Scheme} (emb : X ⟶ TA'.X.left) : BR_affine TA' emb = BR_affine TA (CategoryTheory.CategoryStruct.comp emb φ)

BR_affine is unchanged along an isomorphism of the ambient triples, granted that the principalization sequences correspond: if BP TA' = (BP TA).pullback φ for an isomorphism φ of the ambients and TA'.I = TA.I.comap φ, then BR_affine TA' emb = BR_affine TA (emb ≫ φ). The first-centre index is the same (firstCenterIndex_pullback_of_isIso), and truncation commutes with the pullback. The hypothesis is [Kol07, Theorem 35 (4)] for the smooth surjection φ, supplied in Hironaka.Resolution.Algebraic.Kol07.Thm36.Assembly.