The new chain coordinates at a point of the blow-up

The second half of the local computation for the statement CP4 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) at a point q of the blow-up, on the chart datum ChartAt of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Chart:

• the new parameters (newExp, exists_isUnit_mul_monomialOf_newExp): an ε-power times a monomial in the ε-free induced coordinates is a unit times a monomial in the new regular system of parameters z', the exponents transported along τ (the ratio coordinates of members whose strict transform misses q are units and drop);
• the members' strict transforms at q (stalkIdeal_strictTransformAlong_eq_span_w, stalkIdeal_strictTransformAlong_eq_top_of_isUnit, the dichotomy mem_support_strictTransformAlong_iff);
• the assembly (chainCoords_totalTransform): the new members' coordinates newMemberIdx, the new chain newChain = τ ∘ σ, snc data for the total transform (isSncAt_totalTransform), the support of the new exponents — chain coordinates at q for the total transform of the boundary and the strict transform of Γ;
• the transforms in the new parameters (stalkIdeal_markedTransform_chainKIdeal, stalkIdeal_markedTransform_chainIdeal): the K-shape and the un-isolated form at q;
• off the exceptional divisor (chainRelativeKAt_totalTransform_of_notMem, chainRelativeAt_totalTransform_of_notMem, exists_isSncAt_totalTransform_of_notMem): the forms transport along the stalk isomorphism π^*.

The chart is that of [Kol07, Definition 60]. The pointwise statements are assembled into CP4 in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4; Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP4Sheaf uses them for the un-isolated ideal.

From the induced coordinates to the new regular system of parameters

noncomputable def Hironaka.Resolution.ChartAt.pivotIdx {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (hq : q ∈ (Z.comap Z.blowUpπ).support) : Fin D.m

The pivot's entry among the parameters.

Equations

• D.pivotIdx hq = D.τ ⟨D.c₀, ⋯⟩

theorem Hironaka.Resolution.ChartAt.z'_pivotIdx {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (hq : q ∈ (Z.comap Z.blowUpπ).support) : D.z' (D.pivotIdx hq) = D.ε

noncomputable def Hironaka.Resolution.ChartAt.newExp {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (t : ℕ) (c : Fin n → ℕ) : Fin D.m → ℕ

The exponent vector on the new parameters: the entry t at the pivot, the entries of c at the vanishing induced coordinates, 0 elsewhere.

Equations

• D.newExp t c = Function.extend D.τ (fun (k : { i : Fin n // D.w i ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q) }) => if ↑k = D.c₀ then t else c ↑k) 0

theorem Hironaka.Resolution.ChartAt.monomialOf_z'_extend {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (g : { i : Fin n // D.w i ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q) } → ℕ) : monomialOf D.z' (Function.extend D.τ g 0) = ∏ k : { i : Fin n // D.w i ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q) }, D.w ↑k ^ g k

A monomial in the new parameters with exponents extended along τ is the product over the vanishing induced coordinates.

theorem Hironaka.Resolution.ChartAt.exists_isUnit_mul_monomialOf_newExp {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (hq : q ∈ (Z.comap Z.blowUpπ).support) (t : ℕ) (c : Fin n → ℕ) : ∃ (u : ↑(Z.blowUp.presheaf.stalk q)), IsUnit u ∧ D.ε ^ t * monomialOf D.wHat c = u * monomialOf D.z' (D.newExp t c)

Units drop: ε^t · ŵ^c is a unit times the monomial in the new parameters with the exponents newExp t c.

The strict transforms of the members in the chart

theorem Hironaka.Resolution.ChartAt.stalkIdeal_strictTransformAlong_eq_span_w {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) {c : Fin n} (hc : c ≠ D.c₀) (hcm : D.w c ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) (Y : X.IdealSheafData) (hY : Y.stalkIdeal (Z.blowUpπ q) = Ideal.span {z c}) : (Y.strictTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ)).stalkIdeal q = Ideal.span {D.w c}

A member through q: for a member Y = (z_c = 0) at p whose coordinate is not the pivot and whose induced coordinate vanishes at q, the strict transform has stalk (w_c) at q.

theorem Hironaka.Resolution.ChartAt.stalkIdeal_strictTransformAlong_eq_top_of_isUnit {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {c : Fin n} (hc : c ≠ D.c₀) (hcC : c ∈ C) (hcu : IsUnit (D.w c)) (Y : X.IdealSheafData) (hY : Y.stalkIdeal (Z.blowUpπ q) = Ideal.span {z c}) : (Y.strictTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ)).stalkIdeal q = ⊤

A member missing q: a member Y = (z_c = 0) of the centre (c ∈ C, not the pivot) whose induced coordinate is a unit at q has strict transform missing q.

theorem Hironaka.Resolution.ChartAt.w_mem_maximalIdeal_of_notMem' {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hz : IsLocalRing.IsRegularSystemOfParameters z) {c : Fin n} (hcC : c ∉ C) : D.w c ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)

Off the centre every coordinate's induced coordinate vanishes at q.

theorem Hironaka.Resolution.ChartAt.mem_support_strictTransformAlong_iff {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hz : IsLocalRing.IsRegularSystemOfParameters z) {c : Fin n} (Y : X.IdealSheafData) (hY : Y.stalkIdeal (Z.blowUpπ q) = Ideal.span {z c}) : q ∈ (Y.strictTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ)).support ↔ c ≠ D.c₀ ∧ D.w c ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)

The dichotomy for a member Y = (z_c = 0) through p: q lies on its strict transform iff c is not the pivot and w_c vanishes at q; then the stalk is (w_c).

The new chain coordinates at a point of the exceptional divisor

noncomputable def Hironaka.Resolution.ChartAt.newMemberIdx {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) (hq : q ∈ (Z.comap Z.blowUpπ).support) (j' : (E.totalTransform Z).ι) : Fin D.m

The coordinate assigned to a member of the total transform at q: the parameter of the induced coordinate of a strict transform through q, the pivot's parameter for F (and, irrelevantly, for a strict transform missing q).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Resolution.ChartAt.newMemberIdx_inl {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) (hq : q ∈ (Z.comap Z.blowUpπ).support) (j : E.ι) : D.newMemberIdx E c hq (toLex (Sum.inl j)) = if h : ∃ (hj : Z.blowUpπ q ∈ (E.component j).support), D.w (c ⟨j, hj⟩) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q) then D.τ ⟨c ⟨j, ⋯⟩, ⋯⟩ else D.pivotIdx hq

theorem Hironaka.Resolution.ChartAt.newMemberIdx_inr {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) (hq : q ∈ (Z.comap Z.blowUpπ).support) (u : PUnit.{u + 1}) : D.newMemberIdx E c hq (toLex (Sum.inr u)) = D.pivotIdx hq

theorem Hironaka.Resolution.ChartAt.σ_ne_c₀ {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (Γ : X.IdealSheafData) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hΓ : Γ.stalkIdeal (Z.blowUpπ q) = Ideal.span (Set.range (z ∘ σ))) (hqΓ : q ∈ (Γ.strictTransform Z).support) (i : Fin (r + 1)) : σ i ≠ D.c₀

The pivot is not a chain coordinate when q lies on the strict transform of Γ.

theorem Hironaka.Resolution.ChartAt.w_σ_mem_and_stalkIdeal_strictTransform {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (Γ : X.IdealSheafData) {r : ℕ} (σ : Fin (r + 1) → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hΓ : Γ.stalkIdeal (Z.blowUpπ q) = Ideal.span (Set.range (z ∘ σ))) (hqΓ : q ∈ (Γ.strictTransform Z).support) : (∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) ∧ (Γ.strictTransform Z).stalkIdeal q = Ideal.span (Set.range fun (i : Fin (r + 1)) => D.w (σ i))

The chain coordinates vanish at q and generate the strict transform of Γ there.

noncomputable def Hironaka.Resolution.ChartAt.newChain {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) (i : Fin (r + 1)) : Fin D.m

The new chain: the parameters of the chain coordinates.

Equations

• D.newChain σ hmem i = D.τ ⟨σ i, ⋯⟩

theorem Hironaka.Resolution.ChartAt.z'_newChain {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) (i : Fin (r + 1)) : D.z' (D.newChain σ hmem i) = D.w (σ i)

theorem Hironaka.Resolution.ChartAt.newChain_injective {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσ : Function.Injective σ) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) : Function.Injective (D.newChain σ hmem)

theorem Hironaka.Resolution.ChartAt.exists_of_mem_support_inl {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) (j : E.ι) (hj' : q ∈ ((E.totalTransform Z).component (toLex (Sum.inl j))).support) : ∃ (hj : Z.blowUpπ q ∈ (E.component j).support), c ⟨j, hj⟩ ≠ D.c₀ ∧ D.w (c ⟨j, hj⟩) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)

A member of the total transform through q of the form inl j: j passes through p, its coordinate is not the pivot and its induced coordinate vanishes at q.

theorem Hironaka.Resolution.ChartAt.newMemberIdx_inl_of_mem {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) (j : E.ι) (hj' : q ∈ ((E.totalTransform Z).component (toLex (Sum.inl j))).support) : ∃ (hj : Z.blowUpπ q ∈ (E.component j).support) (hm : D.w (c ⟨j, hj⟩) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)), c ⟨j, hj⟩ ≠ D.c₀ ∧ D.newMemberIdx E c hq (toLex (Sum.inl j)) = D.τ ⟨c ⟨j, hj⟩, hm⟩

The coordinate of a strict transform through q.

theorem Hironaka.Resolution.ChartAt.stalkIdeal_component_inl {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) (j : E.ι) (hj' : q ∈ ((E.totalTransform Z).component (toLex (Sum.inl j))).support) : ((E.totalTransform Z).component (toLex (Sum.inl j))).stalkIdeal q = Ideal.span {D.z' (D.newMemberIdx E c hq (toLex (Sum.inl j)))}

The stalk of a strict transform through q is generated by its new coordinate.

theorem Hironaka.Resolution.ChartAt.stalkIdeal_component_inr {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) (hq : q ∈ (Z.comap Z.blowUpπ).support) (u : PUnit.{u + 1}) : ((E.totalTransform Z).component (toLex (Sum.inr u))).stalkIdeal q = Ideal.span {D.z' (D.newMemberIdx E c hq (toLex (Sum.inr u)))}

The stalk of the exceptional divisor is generated by the pivot's parameter.

theorem Hironaka.Resolution.ChartAt.newMemberIdx_injective {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hcinj : Function.Injective c) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) : Function.Injective fun (j' : { j' : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j').support }) => D.newMemberIdx E c hq ↑j'

The new coordinates of the members through q are distinct.

theorem Hironaka.Resolution.ChartAt.stalkIdeal_component {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) (j' : { j' : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j').support }) : ((E.totalTransform Z).component ↑j').stalkIdeal q = Ideal.span {D.z' (D.newMemberIdx E c hq ↑j')}

Every member of the total transform through q is generated by its new coordinate.

theorem Hironaka.Resolution.ChartAt.isSncAt_totalTransform {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hcinj : Function.Injective c) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) : (E.totalTransform Z).IsSncAt q D.z'

The new coordinates form snc data for the total transform at q.

theorem Hironaka.Resolution.ChartAt.exists_of_newExp_ne_zero {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (t : ℕ) (cc : Fin n → ℕ) {k' : Fin D.m} (h : D.newExp t cc k' ≠ 0) : ∃ (kk : Fin n) (hk : D.w kk ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)), k' = D.τ ⟨kk, hk⟩ ∧ (if kk = D.c₀ then t else cc kk) ≠ 0

A nonzero entry of newExp t c sits at the parameter of a vanishing induced coordinate.

theorem Hironaka.Resolution.ChartAt.newExp_support {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) (t : ℕ) (cc : Fin n → ℕ) (hcc : ∀ (kk : Fin n), cc kk ≠ 0 → kk ∈ Set.range c) (k' : Fin D.m) (h : D.newExp t cc k' ≠ 0) : k' ∈ Set.range fun (j' : { j' : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j').support }) => D.newMemberIdx E c hq ↑j'

The new exponents are supported on the new members' coordinates.

theorem Hironaka.Resolution.ChartAt.newChain_ne_newMemberIdx {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hz : IsLocalRing.IsRegularSystemOfParameters z) (hc : ∀ (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (Z.blowUpπ q) = Ideal.span {z (c j)}) (hσc : ∀ (i : Fin (r + 1)) (j : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support }), σ i ≠ c j) (hσc₀ : ∀ (i : Fin (r + 1)), σ i ≠ D.c₀) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) (i : Fin (r + 1)) (j' : { j' : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j').support }) : D.newChain σ hmem i ≠ D.newMemberIdx E c hq ↑j'

The new chain avoids the new members' coordinates.

theorem Hironaka.Resolution.ChartAt.chainCoords_totalTransform {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) (E : X.DivisorFamily) (Γ : X.IdealSheafData) (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] [IsRegularLocalRing ↑(X.presheaf.stalk (Z.blowUpπ q))] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hcoords : ChainCoords E Γ (Z.blowUpπ q) z c σ a) (hqΓ : q ∈ (Γ.strictTransform Z).support) (Dexp : Fin (r + 1) → ℕ) : ChainCoords (E.totalTransform Z) (Γ.strictTransform Z) q D.z' (fun (j' : { j : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j).support }) => D.newMemberIdx E c hq ↑j') (D.newChain σ ⋯) fun (i : Fin (r + 1)) => D.newExp (Dexp i) (a i)

The new chain coordinates at q: the parameters z', the members' coordinates, the chain τ ∘ σ and the exponents newExp (D_i) (a_i).

The transforms in the new parameters

theorem Hironaka.Resolution.ChartAt.wHat_comp_eq {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {r : ℕ} (σ : Fin (r + 1) → Fin n) (hσc₀ : ∀ (i : Fin (r + 1)), σ i ≠ D.c₀) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) : (fun (i : Fin (r + 1)) => D.wHat (σ i)) = D.z' ∘ D.newChain σ hmem

The ε-free chain equations are the new chain's parameters.

theorem Hironaka.Resolution.ChartAt.stalkIdeal_markedTransform_chainKIdeal {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hσc₀ : ∀ (i : Fin (r + 1)), σ i ≠ D.c₀) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) (b : Fin n → ℕ) (K : X.IdealSheafData) (hK : K.stalkIdeal (Z.blowUpπ q) = Ideal.span {monomialOf z b} * chainKIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (δ : Fin (r + 1) → ℕ) (hδ : ∀ (i : Fin (r + 1)), δ i = if σ i ∈ C then 1 else 0) (hpos : 1 ≤ epsOrderC C a b (Function.update δ (Fin.last r) 0) 0) (hmono : ∀ (i : Fin r), epsOrderC C a b (Function.update δ (Fin.last r) 0) i.castSucc ≤ epsOrderC C a b (Function.update δ (Fin.last r) 0) i.succ) (Dexp : Fin (r + 1) → ℕ) (hD : ∀ (i : Fin r), Dexp i.castSucc = epsOrderC C a b (Function.update δ (Fin.last r) 0) i.succ - epsOrderC C a b (Function.update δ (Fin.last r) 0) i.castSucc) : (K.markedTransform Z 1).stalkIdeal q = Ideal.span {monomialOf D.z' (D.newExp (epsOrderC C a b (Function.update δ (Fin.last r) 0) 0 - 1) b)} * chainKIdeal (D.z' ∘ D.newChain σ hmem) fun (i : Fin (r + 1)) => monomialOf D.z' (D.newExp (Dexp i) (a i))

The K-shape in the new parameters: under the ε-order conditions (the admissibility condition (★)), the mark-1 transform of a K-shape is the K-shape with chain τ ∘ σ, level exponents newExp (D_i) (a_i) and top exponents newExp (E_0 − 1) b.

theorem Hironaka.Resolution.ChartAt.stalkIdeal_markedTransform_chainIdeal {X : AlgebraicGeometry.Scheme} {Z : X.IdealSheafData} {q : ↥Z.blowUp} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} {C : Finset (Fin n)} (D : ChartAt Z q z C) {r : ℕ} (σ : Fin (r + 1) → Fin n) (a : Fin (r + 1) → Fin n → ℕ) [IsRegularLocalRing ↑(Z.blowUp.presheaf.stalk q)] (hq : q ∈ (Z.comap Z.blowUpπ).support) (hσc₀ : ∀ (i : Fin (r + 1)), σ i ≠ D.c₀) (hmem : ∀ (i : Fin (r + 1)), D.w (σ i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk q)) (b : Fin n → ℕ) (I : X.IdealSheafData) (hI : I.stalkIdeal (Z.blowUpπ q) = Ideal.span {monomialOf z b} * chainIdeal (z ∘ σ) fun (i : Fin (r + 1)) => monomialOf z (a i)) (δ : Fin (r + 1) → ℕ) (hδ : ∀ (i : Fin (r + 1)), δ i = if σ i ∈ C then 1 else 0) (hpos : 1 ≤ epsOrderC C a b δ 0) (hmono : ∀ (i : Fin r), epsOrderC C a b δ i.castSucc ≤ epsOrderC C a b δ i.succ) (Dexp : Fin (r + 1) → ℕ) (hD : ∀ (i : Fin r), Dexp i.castSucc = epsOrderC C a b δ i.succ - epsOrderC C a b δ i.castSucc) : (I.markedTransform Z 1).stalkIdeal q = Ideal.span {monomialOf D.z' (D.newExp (epsOrderC C a b δ 0 - 1) b)} * chainIdeal (D.z' ∘ D.newChain σ hmem) fun (i : Fin (r + 1)) => monomialOf D.z' (D.newExp (Dexp i) (a i))

The un-isolated form in the new parameters.

Off the exceptional divisor: transport along the stalk isomorphism

noncomputable def Hironaka.Resolution.offCentreIdx {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} {n : ℕ} (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) (j' : (E.totalTransform Z).ι) : Fin n

The members' coordinates transported to the total transform (the exceptional divisor and the strict transforms missing q receive an irrelevant value).

Equations

• Hironaka.Resolution.offCentreIdx E Z c σ j' = Sum.elim (fun (j : E.ι) => if h : Z.blowUpπ q ∈ (E.component j).support then c ⟨j, h⟩ else σ 0) (fun (x : PUnit.{?u.1 + 1}) => σ 0) (ofLex j')

theorem Hironaka.Resolution.offCentreIdx_inl_of_mem {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} {n : ℕ} (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) (j : E.ι) (hj : Z.blowUpπ q ∈ (E.component j).support) : offCentreIdx E Z c σ (toLex (Sum.inl j)) = c ⟨j, hj⟩

theorem Hironaka.Resolution.mem_support_totalTransform_component_iff {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (j : E.ι) : q ∈ ((E.totalTransform Z).component (toLex (Sum.inl j))).support ↔ Z.blowUpπ q ∈ (E.component j).support

Off the exceptional divisor a strict transform passes through q iff the member passes through π(q); the exceptional divisor misses q.

theorem Hironaka.Resolution.not_mem_support_totalTransform_component_inr {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (u : PUnit.{u + 1}) : q ∉ ((E.totalTransform Z).component (toLex (Sum.inr u))).support

theorem Hironaka.Resolution.stalkIdeal_totalTransform_component_inl {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (j : E.ι) : ((E.totalTransform Z).component (toLex (Sum.inl j))).stalkIdeal q = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) ((E.component j).stalkIdeal (Z.blowUpπ q))

The stalk of a strict transform off the exceptional divisor is the image of the member's stalk under the stalk isomorphism.

theorem Hironaka.Resolution.stalkIdeal_strictTransform_eq_map_of_notMem {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (Γ : X.IdealSheafData) : (Γ.strictTransform Z).stalkIdeal q = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (Γ.stalkIdeal (Z.blowUpπ q))

The stalk of the strict transform of Γ off the exceptional divisor.

theorem Hironaka.Resolution.stalkIdeal_markedTransform_one_of_notMem {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (K : X.IdealSheafData) : (K.markedTransform Z 1).stalkIdeal q = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (K.stalkIdeal (Z.blowUpπ q))

The stalk of the mark-1 transform off the exceptional divisor is the image of the stalk.

theorem Hironaka.Resolution.chainCoords_totalTransform_of_notMem {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) {Γ : X.IdealSheafData} {a : Fin (r + 1) → Fin n → ℕ} (hcoords : ChainCoords E Γ (Z.blowUpπ q) z c σ a) : ChainCoords (E.totalTransform Z) (Γ.strictTransform Z) q (fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) (z i)) (fun (j' : { j : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j).support }) => offCentreIdx E Z c σ ↑j') σ a

The chain-relative form (K-shape) transports off the exceptional divisor: coordinates π^* z, the same chain and exponents.

theorem Hironaka.Resolution.range_le_range_offCentreIdx {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) {n : ℕ} (c : { j : E.ι // Z.blowUpπ q ∈ (E.component j).support } → Fin n) {r : ℕ} (σ : Fin (r + 1) → Fin n) (k : Fin n) (hk : k ∈ Set.range c) : k ∈ Set.range fun (j' : { j' : (E.totalTransform Z).ι // q ∈ ((E.totalTransform Z).component j').support }) => offCentreIdx E Z c σ ↑j'

The support of the exponents transports off the exceptional divisor.

theorem Hironaka.Resolution.chainRelativeKAt_totalTransform_of_notMem {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (K Γ : X.IdealSheafData) (h : ChainRelativeKAt E K Γ (Z.blowUpπ q)) : ChainRelativeKAt (E.totalTransform Z) (K.markedTransform Z 1) (Γ.strictTransform Z) q

CP4 off the exceptional divisor, K-shape: the K-shape transports along the stalk isomorphism at a point off the centre.

theorem Hironaka.Resolution.chainRelativeAt_totalTransform_of_notMem {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (I Γ : X.IdealSheafData) (h : ChainRelativeAt E I Γ (Z.blowUpπ q)) : ChainRelativeAt (E.totalTransform Z) (I.markedTransform Z 1) (Γ.strictTransform Z) q

CP4 off the exceptional divisor, un-isolated form.

theorem Hironaka.Resolution.exists_isSncAt_totalTransform_of_notMem {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (Z : X.IdealSheafData) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) (Γ : X.IdealSheafData) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ q))} (hsnc : E.IsSncAt (Z.blowUpπ q) z) {s : Finset (Fin n)} (hΓ : Γ.stalkIdeal (Z.blowUpπ q) = Ideal.span (z '' ↑s)) : ∃ (z' : Fin n → ↑(Z.blowUp.presheaf.stalk q)), (E.totalTransform Z).IsSncAt q z' ∧ (Γ.strictTransform Z).stalkIdeal q = Ideal.span (z' '' ↑s)

snc data off the exceptional divisor: Γ̃ has snc with the total transform at q when Γ has snc with E at π(q).