The sheaf forms of one blow-up along an admissible chain stratum

The statement CP4 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative; Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4) in the form that CP6 consumes: with I = Γ ⊓ K (or I = (⨅ γ ∈ Γs, γ) ⊓ K for pairwise disjoint protected components), the mark-1 transform of I along the blow-up of an admissible chain stratum is the meet of the strict transform(s) with the mark-1 transform of K, as ideal sheaves on the whole blow-up.

The proof. Ideal sheaves are compared stalk by stalk (ext_stalkIdeal). At q over p ∉ Γ both sides are the mark-1 transform of K (I_p = K_p, the locality of the marked transform, and Γ̃_q = 𝒪). At q over p ∈ Γ off the exceptional divisor everything is the image under the stalk isomorphism π^*, which preserves meets. At q ∈ F over p ∈ Z ∩ Γ the K-shape of K_p and the intersection form span_mul_chainIdeal_eq_span_inf of Hironaka.Resolution.Algebraic.Wlo05.ChainIdealInf give I_p its un-isolated form; the chart computation of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4 transports both forms to q; if q ∈ Γ̃, the intersection form at q in the new parameters is the identity; if q ∉ Γ̃ some transported chain equation is a unit at q (the charts of the chain equations, and the points off Γ̃ of the charts of the members), and chainIdeal_eq_chainKIdeal_of_isUnit gives Ĩ_q = K̃_q while Γ̃_q = 𝒪. For the finset form the meet of the members has, at every point, the stalk of the one member through it or 𝒪 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Tools), on X and on the blow-up (strict transforms of disjoint members are disjoint). The chart is that of Kol07, Definition 60. These statements are not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Stage, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5.

The pointwise identity

theorem Hironaka.Resolution.stalkIdeal_markedTransform_inf_of_notMem {X : AlgebraicGeometry.Scheme} (Γ K Z : X.IdealSheafData) [AlgebraicGeometry.IsLocallyNoetherian X] {q : ↥Z.blowUp} (hp : Z.blowUpπ q ∉ Γ.support) : ((Γ ⊓ K).markedTransform Z 1).stalkIdeal q = (K.markedTransform Z 1).stalkIdeal q

Off Γ the mark-1 transform of Γ ⊓ K is that of K.

theorem Hironaka.Resolution.map_inf_stalkMapπEquiv {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (A B : Ideal ↑(X.presheaf.stalk (Z.blowUpπ q))) : Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (A ⊓ B) = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) A ⊓ Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) B

The image of a meet under the stalk isomorphism off the exceptional divisor.

theorem Hironaka.Resolution.stalkIdeal_markedTransform_inf_of_mem {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (Γ K Z : X.IdealSheafData) {q : ↥Z.blowUp} (hpΓ : Z.blowUpπ q ∈ Γ.support) (hZ : ∀ p ∈ Z.support ⊓ Γ.support, AdmissibleChainStratumKAt E K Γ Z p) : ((Γ ⊓ K).markedTransform Z 1).stalkIdeal q = (Γ.strictTransform Z).stalkIdeal q ⊓ (K.markedTransform Z 1).stalkIdeal q

The pointwise sheaf identity at a point over Γ: for p ∈ Γ, with the K-shape of K at p and admissibility at p when p ∈ Z, and the snc data of Z along Z ∩ Γ (for the regularity of the stalks of the blow-up).

theorem Hironaka.Resolution.disjoint_strictTransform_support_of_disjoint {X : AlgebraicGeometry.Scheme} (Z a b : X.IdealSheafData) (h : Disjoint a.support b.support) : Disjoint (a.strictTransform Z).support (b.strictTransform Z).support

Disjoint members have disjoint strict transforms (the strict transform lies over the member).

The two sheaf identities

theorem Hironaka.Resolution.markedTransform_inf_of_admissible {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (I K Γ Z : X.IdealSheafData) (hE : E.IsSnc) (hΓ : E.HasSncWith Γ) (hsm : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Γ.subschemeι f)) (hI : I = Γ ⊓ K) (hK : ∀ p ∈ Γ.support, ChainRelativeKAt E K Γ p) (hZ : ∀ p ∈ Z.support ⊓ Γ.support, AdmissibleChainStratumKAt E K Γ Z p) (hKZ : K ≤ Z) : I.markedTransform Z 1 = Γ.strictTransform Z ⊓ K.markedTransform Z 1

The single-blow-up sheaf form of CP4 for the pair (I, K): with I = Γ ⊓ K on X, K in the K-shape along Γ, Z admissible at every point of Z ∩ Γ, and the order condition K ≤ Z of the run (a GLOBAL condition needed off Γ; not the admissibility condition (★)), the mark-1 transform of I is the intersection of the strict transform of Γ with the mark-1 transform of K, as ideal sheaves on the whole blow-up.

theorem Hironaka.Resolution.markedTransform_biInf_inf_of_admissible {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (I K Z : X.IdealSheafData) (Γs : Finset X.IdealSheafData) (hE : E.IsSnc) (hΓ : ∀ γ ∈ Γs, E.HasSncWith γ) (hsm : ∀ γ ∈ Γs, AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp γ.subschemeι f)) (hdisj : (↑Γs).Pairwise fun (a b : X.IdealSheafData) => Disjoint a.support b.support) (hI : I = (⨅ γ ∈ Γs, γ) ⊓ K) (hK : ∀ γ ∈ Γs, ∀ p ∈ γ.support, ChainRelativeKAt E K γ p) (hZ : ∀ γ ∈ Γs, ∀ p ∈ Z.support ⊓ γ.support, AdmissibleChainStratumKAt E K γ Z p) (hKZ : K ≤ Z) : I.markedTransform Z 1 = (⨅ γ ∈ Γs, γ.strictTransform Z) ⊓ K.markedTransform Z 1

The finset form of the sheaf identity (the blow-up step of CP6 for the SET of protected components): with I = (⨅ γ ∈ Γs, γ) ⊓ K, pairwise disjoint protected components Γs, each K-admissible along Z, and K ≤ Z, the mark-1 transform of I is the meet of the strict transforms with the mark-1 transform of K.