The algebra of birational transforms of marked ideals under one blowing-up

Marked ideals (I, m) multiply with their marks adding and add for a common mark [Kol07, Definition 59], and the birational transform π_*^{-1}(I, m) = (I_F^{-m} π^*I, m) [Kol07, Definition 60] is defined when m ≤ ord_Y I along the centre. This file proves the rules that the proof of the tuning theorem [Kol07, Theorem 100] uses at every step: for marked ideal sheaves whose transforms are defined, the birational transform of a product is the product of the birational transforms, of a power the power, of a same-mark sum the sum, and the birational transform grows with the mark. They are the analytic counterparts of the rules for schemes in Hironaka.Resolution.Algebraic.Tuning.Transform (markedTransform_mul, markedTransform_finset_prod, markedTransform_iSup_eq) and Hironaka.Resolution.Algebraic.Kol07.Tuning (markedTransform_pow), for MarkedIdealSheaf.birationalTransform.

The argument

The birational transform is the classical choice of an ideal sheaf with the colon stalks (π⁻¹(J)_{a'} : I_{F,a'}^k), characterised by isDivExceptional_birationalTransform under the divisibility k ≤ ord_Y J along the centre, so every rule carries that hypothesis for every marked ideal sheaf involved, and the rules are proved stalkwise:

• over the centre, in a blow-up chart of index i, the exceptional ideal is generated by the scaling coordinate u = u_i (stalkIdeal_exceptionalIdealSheaf_eq_span_coord), the stalk is a domain (isDomain_stalk) and u ≠ 0, and the divisibility gives π⁻¹(J)_{a'} ⊆ (u^k) (totalTransform_stalkIdeal_le); the colon algebra of a domain then does the rest: for A ⊆ (u^a), B ⊆ (u^b), (A B : u^{a+b}) = (A : u^a)(B : u^b), (A^s : u^{ks}) = (A : u^k)^s, (A + B : u^k) = (A : u^k) + (B : u^k) (exact division: A = u^a (A : u^a) and (u^k C : u^k) = C), and (A : u^s) ⊆ (A : u^t) for s ≤ t;
• off the centre the birational transform is the total transform (birationalTransform_stalkIdeal_of_notMem) and the rules are the multiplicativity of Ideal.map (Ideal.map_mul, Ideal.map_pow, Ideal.map_sup).

The definedness of the products, powers and sums themselves is the order bookkeeping along the centre (le_ordAlongIdeal_mul, le_ordAlongIdeal_pow, le_ordAlongIdeal_finset_sum, le_ordAlongIdeal_finset_prod), the analogue along Y of the cosupport rules (1)–(4) of [Kol07, Definition 59], read on the stalk containments J_a ⊆ D_a^p of IdealSheaf.ordAlongIdeal. The colon algebra of a domain is elementary (the quotient is independent of the generators, Ideal.colon_span_range_pow_mul). The rules are used by the tuning computation of Hironaka.Manifold.BlowUp.Transform.TuningTransform.

Orders along a centre under products, powers and sums (Kollár 59.1–59.4 along Y)

theorem Manifold.le_ordAlongIdeal_mul {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) {a : ↑X} {J K : IdealSheaf 𝒪} {p q : ℕ} (hp : ↑p ≤ D.ordAlongIdeal J a) (hq : ↑q ≤ D.ordAlongIdeal K a) : ↑(p + q) ≤ D.ordAlongIdeal (J * K) a

ord_D (J K) ≥ ord_D J + ord_D K — J_a ⊆ D_a^p and K_a ⊆ D_a^q give (JK)_a ⊆ D_a^{p+q}.

theorem Manifold.le_ordAlongIdeal_pow {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) {a : ↑X} {J : IdealSheaf 𝒪} {p : ℕ} (hp : ↑p ≤ D.ordAlongIdeal J a) (s : ℕ) : ↑(p * s) ≤ D.ordAlongIdeal (J ^ s) a

ord_D (J^s) ≥ s · ord_D J.

theorem Manifold.le_ordAlongIdeal_finset_sum {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) {a : ↑X} {ι : Type u_1} (F : Finset ι) (G : ι → IdealSheaf 𝒪) {p : ℕ} (hG : ∀ i ∈ F, ↑p ≤ D.ordAlongIdeal (G i) a) : ↑p ≤ D.ordAlongIdeal (∑ i ∈ F, G i) a

A finite sum of ideal sheaves of order ≥ p along D has order ≥ p along D.

theorem Manifold.le_ordAlongIdeal_finset_prod {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D : IdealSheaf 𝒪) {a : ↑X} {ι : Type u_1} (F : Finset ι) (G : ι → IdealSheaf 𝒪) (c : ι → ℕ) (hG : ∀ i ∈ F, ↑(c i) ≤ D.ordAlongIdeal (G i) a) : ↑(∑ i ∈ F, c i) ≤ D.ordAlongIdeal (∏ i ∈ F, G i) a

A finite product of ideal sheaves of orders ≥ c_i along D has order ≥ ∑ c_i along D.

The marked transform under one blowing-up: products, powers, sums, marks

theorem Manifold.birationalTransform_stalkIdeal_eq_colon_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {J : IdealSheaf (structureSheaf 𝕜 E M)} {k : ℕ} (hk : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J x) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) : (MarkedIdealSheaf.birationalTransform hY h { I := J, m := k }).I.stalkIdeal p = Submodule.colon ((IdealSheaf.pullback π ⋯ J).stalkIdeal p) {coord E ψ Φ ⋯ hp (σ i) ^ k}

At a point p of a blow-up chart of index i, the stalk of the marked transform of (J, k) is the colon of the total transform's stalk by the k-th power of the scaling coordinate u_i.

theorem Manifold.totalTransform_stalkIdeal_le_span_coord_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {J : IdealSheaf (structureSheaf 𝕜 E M)} {k : ℕ} (hk : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J x) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) (hpY : π p ∈ Y) : (IdealSheaf.pullback π ⋯ J).stalkIdeal p ≤ Ideal.span {coord E ψ Φ ⋯ hp (σ i) ^ k}

At a point over the centre, the total transform's stalk lies in the ideal of the k-th power of the scaling coordinate.

theorem Manifold.birationalTransform_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (J₁ J₂ : IdealSheaf (structureSheaf 𝕜 E M)) (a b : ℕ) (h₁ : ∀ x ∈ Y, ↑a ≤ hY.idealSheaf.ordAlongIdeal J₁ x) (h₂ : ∀ x ∈ Y, ↑b ≤ hY.idealSheaf.ordAlongIdeal J₂ x) : (MarkedIdealSheaf.birationalTransform hY h { I := J₁ * J₂, m := a + b }).I = (MarkedIdealSheaf.birationalTransform hY h { I := J₁, m := a }).I * (MarkedIdealSheaf.birationalTransform hY h { I := J₂, m := b }).I

For marked ideal sheaves (J₁, a), (J₂, b) whose transforms are defined — a ≤ ord_Y J₁, b ≤ ord_Y J₂ along Y — the marked transform of (J₁ J₂, a + b) is the product of the marked transforms: stalkwise, (π⁻¹(J₁) π⁻¹(J₂) : u^{a+b}) = (π⁻¹(J₁) : u^a) · (π⁻¹(J₂) : u^b) for the exceptional coordinate u (exact division in the domain 𝒪_{M',p}), and the identity off the centre.

theorem Manifold.birationalTransform_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (J : IdealSheaf (structureSheaf 𝕜 E M)) (k s : ℕ) (hk : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J x) : (MarkedIdealSheaf.birationalTransform hY h { I := J ^ s, m := k * s }).I = (MarkedIdealSheaf.birationalTransform hY h { I := J, m := k }).I ^ s

For a marked ideal sheaf (J, k) whose transform is defined, the marked transform of (J^s, ks) is the s-th power of the marked transform.

theorem Manifold.birationalTransform_add {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (J₁ J₂ : IdealSheaf (structureSheaf 𝕜 E M)) (k : ℕ) (h₁ : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J₁ x) (h₂ : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J₂ x) : (MarkedIdealSheaf.birationalTransform hY h { I := J₁ + J₂, m := k }).I = (MarkedIdealSheaf.birationalTransform hY h { I := J₁, m := k }).I + (MarkedIdealSheaf.birationalTransform hY h { I := J₂, m := k }).I

For marked ideal sheaves (J₁, k), (J₂, k) whose transforms are defined, the marked transform of (J₁ + J₂, k) is the sum of the marked transforms (the sum of ideal sheaves, stalkwise ⊔).

theorem Manifold.birationalTransform_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) : (MarkedIdealSheaf.birationalTransform hY h { I := 1, m := 0 }).I = 1

The marked transform of (𝒪, 0) is the unit ideal sheaf.

theorem Manifold.birationalTransform_finset_prod {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {ι : Type u_2} (F : Finset ι) (G : ι → IdealSheaf (structureSheaf 𝕜 E M)) (c✝ : ι → ℕ) (hG : ∀ i ∈ F, ∀ x ∈ Y, ↑(c✝ i) ≤ hY.idealSheaf.ordAlongIdeal (G i) x) : (MarkedIdealSheaf.birationalTransform hY h { I := ∏ i ∈ F, G i, m := ∑ i ∈ F, c✝ i }).I = ∏ i ∈ F, (MarkedIdealSheaf.birationalTransform hY h { I := G i, m := c✝ i }).I

For marked ideal sheaves (G_i, c_i) whose transforms are defined, the marked transform of (∏ G_i, ∑ c_i) is the product of the marked transforms.

theorem Manifold.birationalTransform_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (k : ℕ) : (MarkedIdealSheaf.birationalTransform hY h { I := 0, m := k }).I = 0

The marked transform of (0, k) is the zero ideal sheaf.

theorem Manifold.birationalTransform_finset_sum {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {ι : Type u_2} (F : Finset ι) (G : ι → IdealSheaf (structureSheaf 𝕜 E M)) (k : ℕ) (hG : ∀ i ∈ F, ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal (G i) x) : (MarkedIdealSheaf.birationalTransform hY h { I := ∑ i ∈ F, G i, m := k }).I = ∑ i ∈ F, (MarkedIdealSheaf.birationalTransform hY h { I := G i, m := k }).I

For marked ideal sheaves (G_i, k) of a common mark whose transforms are defined, the marked transform of (∑ G_i, k) is the sum of the marked transforms.

theorem Manifold.birationalTransform_le_of_le_mark {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (J : IdealSheaf (structureSheaf 𝕜 E M)) {s t : ℕ} (hst : s ≤ t) (ht : ∀ x ∈ Y, ↑t ≤ hY.idealSheaf.ordAlongIdeal J x) : (MarkedIdealSheaf.birationalTransform hY h { I := J, m := s }).I ≤ (MarkedIdealSheaf.birationalTransform hY h { I := J, m := t }).I

For s ≤ t ≤ ord_Y J along Y, π_*^{-1}(J, s) ⊆ π_*^{-1}(J, t): the colon by a smaller power of the exceptional ideal is smaller. This is the step Π_*^{-1}(P, ms) ⊆ Π_*^{-1}(P, ∑ (m − j) c_j) for ∑ (m − j) c_j ≥ ms of the proof of [Kol07, Theorem 100].