Going up: naturality of the marked transform under diffeomorphisms

The two naturality statements of the marked transform π_*^{-1}(I, m) [Kol07, Definition 60] from which the identity "the restriction of the push-forward is the given sequence" (Kollár's natural inclusions j_i : S_i ↪ X_i, [Kol07, 30.2–30.3]; markedTransformSeq_pullback_pushforwardIncl in GoingUp/PushforwardTransform.lean) is assembled step by step:

• birationalTransform_pullback_of_comp_eq (invariance): for two blowings-up π₁ : M₁' → M, π₂ : M₂' → M of the same centre Y and a diffeomorphism e : M₁' ≃ M₂' over M (π₂ ∘ e = π₁; the unique diffeomorphism between two blowings-up of one centre [BM88, Definition 4.1], IsBlowUp.diffeomorph), the marked transform along π₂ pulls back along e to the marked transform along π₁. The total transform and the exceptional ideal sheaf are pullbacks (pullback_pullback), the colon stalks characterizing the marked transform correspond along the bijective stalk maps of e (Ideal.map_colon_pow_of_bijective), and the uniqueness of the colon characterization (IsDivExceptional.unique) concludes.
• idealSheaf_image_diffeomorph_pullback, birationalTransform_image_diffeomorph (base change): for a diffeomorphism g : M₁ ≃ M₂ of the base, the ideal sheaf of g(Y) pulls back to the ideal sheaf of Y (comap_idealSheaf_of_isLocalDiffeomorph and the congruence of the ideal sheaves of one set), and the marked transform of (J, k) along the blowing-up g ∘ π : M' → M₂ of g(Y) (IsBlowUp.diffeomorph_comp) is the marked transform of (g^* J, k) along π.

In the step of the push-forward identity, j_{i+1} = ι_{S_{i+1}} ∘ e_{i+1} with e_{i+1} the unique diffeomorphism between the given blowing-up e_i ∘ π_i^T : T_{i+1} → S_i and the restricted blow-down S_{i+1} → S_i (blowUpStep); the one-blowing-up Lemma 62 [Kol07, Lemma 62] handles ι_{S_{i+1}}, the invariance handles e_{i+1}, the base change handles e_i.

Invariance under a diffeomorphism over the base

theorem Hironaka.Manifold.birationalTransform_pullback_of_comp_eq {𝕜 : 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₁' M₂' : Type u} [TopologicalSpace M₁'] [ChartedSpace E M₁'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁'] [T2Space M₁'] [SecondCountableTopology M₁'] [TopologicalSpace M₂'] [ChartedSpace E M₂'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂'] [T2Space M₂'] [SecondCountableTopology M₂'] {π₁ : M₁' → M} {π₂ : M₂' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h₁ : Manifold.IsBlowUp ψ Y c π₁) (h₂ : Manifold.IsBlowUp ψ Y c π₂) (e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤) (he : π₂ ∘ ⇑e = π₁) (J : Manifold.MarkedIdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hm : ∀ a ∈ Y, ↑J.m ≤ hY.idealSheaf.ordAlongIdeal J.I a) : Manifold.IdealSheaf.pullback ⇑e ⋯ (Manifold.MarkedIdealSheaf.birationalTransform hY h₂ J).I = (Manifold.MarkedIdealSheaf.birationalTransform hY h₁ J).I

The marked transform [Kol07, Definition 60] is invariant under a diffeomorphism e : M₁' ≃ M₂' over M between two blowings-up of the centre Y (the unique diffeomorphism of [BM88, Definition 4.1]): the marked transform along π₂ pulls back along e to the marked transform along π₁. The total transform and the exceptional ideal sheaf pull back to each other (pullback_pullback, π₂ ∘ e = π₁), the colon stalks correspond along the bijective stalk maps of e, and the uniqueness of the colon characterization concludes. Not in the sources; an auxiliary lemma.

Base change along a diffeomorphism

theorem Hironaka.Manifold.idealSheaf_image_diffeomorph_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) {Y : Set M₁.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) : Manifold.IdealSheaf.pullback ⇑g ⋯ ⋯.idealSheaf = hY.idealSheaf

The ideal sheaf of the image g(Y) of a closed submanifold under a diffeomorphism pulls back along g to the ideal sheaf of Y (by the uniqueness of the ideal sheaf of a closed submanifold): comap_idealSheaf_of_isLocalDiffeomorph for the preimage g⁻¹(g(Y)) = Y.

theorem Hironaka.Manifold.birationalTransform_image_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M₁ M₂ M' : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) {Y : Set M₁.carrier} {c : ℕ} {π : M'.carrier → M₁.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (J : M₂.IdealSheaf) (k : ℕ) (hk : ∀ a ∈ ⇑g '' Y, ↑k ≤ ⋯.idealSheaf.ordAlongIdeal J a) : (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := J, m := k }).I = (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := Manifold.IdealSheaf.pullback ⇑g ⋯ J, m := k }).I

Base change of the marked transform [Kol07, Definition 60] along a diffeomorphism g : M₁ ≃ M₂ (the centres Z_i^X = (j_i)_* Z_i^S of [Kol07, 30.3]): the marked transform of (J, k) along the blowing-up g ∘ π of g(Y) is the marked transform of (g^* J, k) along the blowing-up π of Y. The total transforms agree (pullback_pullback), the exceptional ideal sheaves agree by idealSheaf_image_diffeomorph_pullback, and the uniqueness of the colon characterization concludes; the marking is legitimate for (g^* J, k) by le_ordAlongIdeal_pullback.