The induction of Kollár's Theorem 97 on lists of centres

Kollár's proof of the uniqueness of blow-up sequences [Kol07, Theorem 97, proof] is an induction on the length of the blow-up sequence: given the local-isomorphism equivalence ψ, ψ' : U ⇉ M with the common pull-back C = ψ^*L = ψ'^*L', C of order ≥ 1 for (MC(ψ^*I), 1), one proves at each stage

1. Z_i = Z'_i: every point of Z_i is ψ_i(u) for some u ∈ Z_i^U ⊆ W_i (the centres lie in the images of the lifts and in the cosupport of the marked transform), and ψ_i(u) = ψ'_i(u) there because ψ_i, ψ'_i agree on V(M_i) — so Z_i ⊆ Z'_i, and symmetrically;
2. X_{i+1} = X'_{i+1} — the blow-up of the same centre — and the pulled-back sequences of the tails are again equal (the lists are compared centre by centre: cons.inj);
3. the lifts ψ_{i+1}, ψ'_{i+1} agree on V(M_{i+1}), M_{i+1} = (π_i^U)^{-1}_*(M_i, 1): the one-step descent lemma agreeOnSubspace_blowUpLift (Hironaka/Resolution/Analytic/MaximalContact/OneStepDescent.lean).

This module proves the induction with the one-step lemma as a hypothesis (hstep), so that the assembly is checked independently of that lemma; Theorem 97 in marked form (eq_of_locallyIsoEquivalentSequences, Hironaka/Resolution/Analytic/MaximalContact/Theorem97Star.lean) is its instance. The list-level bookkeeping:

• BlowUpSequence.eq_nil_of_length_eq_zero: a list of length 0 is nil;
• transport of the second lift along the equality of stages Bl_{ψ⁻¹Y} U = Bl_{ψ'⁻¹Y} U given by ψ⁻¹Y = ψ'⁻¹Y (blowUp_congr, AnalyticMap.castDom — the cast of an analytic map along an equality of its domain, with its lemmas all by subst), which lets the two pulled-back tails be compared as lists over one manifold;
• IsMarkedOne peeled on cons (isMarkedOne_cons_zero, isMarkedOne_cons_tail), the centre clause of the one-step lemma from comap_idealSheaf_of_isLocalDiffeomorph, and the identification of the marked transform of the sequence with the one-step lemma's (cons_markedTransformSeq_one).

Włodarczyk's equivariance of the test blow-ups under the glueing automorphism is the same induction [Wlo09, Lemma 5.5.3 (5)]; the Hironaka library has it for schemes (Hironaka/Resolution/Algebraic/MaximalContact/Theorem97.lean).

Transport of an analytic map along an equality of its domain

def Hironaka.Manifold.AnalyticMap.castDom {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U U' N : AnalyticManifold 𝕜 E} (h : U = U') (f : AnalyticMap U' N) : AnalyticMap U N

The analytic map f : U' → N read on U along h : U = U'.

Equations

• Hironaka.Manifold.AnalyticMap.castDom h f = ⋯ ▸ f

theorem Hironaka.Manifold.AnalyticMap.isLocalDiffeomorph_castDom {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U U' N : AnalyticManifold 𝕜 E} (h : U = U') {f : AnalyticMap U' N} (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(castDom h f)

theorem AnalyticManifold.BlowUpSequence.eq_nil_of_length_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : L.length = 0) : L = nil M

A list of centres of length 0 is the empty list.

theorem AnalyticManifold.BlowUpSequence.blowUp_congr {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z Z' : Set M.carrier} {c : ℕ} (hZZ' : Z = Z') (hZ : Manifold.IsClosedSubmanifold ψ₀ Z c) (hZ' : Manifold.IsClosedSubmanifold ψ₀ Z' c) : Manifold.blowUp ψ₀ hZ = Manifold.blowUp ψ₀ hZ'

Kollár's "X_{i+1} = X'_{i+1}" [Kol07, Theorem 97, proof]: the blow-ups of equal centres are equal.

theorem AnalyticManifold.BlowUpSequence.pullback_castDom_heq {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M U U' : AnalyticManifold 𝕜 E} (h : U = U') (f : AnalyticMap U' M) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (L : BlowUpSequence ψ₀ M) : L.pullback (Hironaka.Manifold.AnalyticMap.castDom h f) ⋯ ≍ L.pullback f hf

The pull-back along a transported map is the transported pull-back.

theorem AnalyticManifold.BlowUpSequence.range_pullbackLift_castDom {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M U U' : AnalyticManifold 𝕜 E} (h : U = U') (f : AnalyticMap U' M) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (L : BlowUpSequence ψ₀ M) (i : Fin (L.length + 1)) : Set.range ⇑(L.pullbackLift (Hironaka.Manifold.AnalyticMap.castDom h f) ⋯ i) = Set.range ⇑(L.pullbackLift f hf i)

The images of the lifts of a transported map are those of the lifts of the map.

theorem AnalyticManifold.BlowUpSequence.blowUpπ_castDom_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {Z : Set N.carrier} {c : ℕ} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hZ : Manifold.IsClosedSubmanifold ψ₀ Z c) (hZg : Z = ⇑g ⁻¹' Y) (q : (Manifold.blowUp ψ₀ hZ).carrier) : (Manifold.blowUpπ ψ₀ hY) ((Hironaka.Manifold.AnalyticMap.castDom ⋯ (liftStep g hg hY)) q) = g ((Manifold.blowUpπ ψ₀ hZ) q)

The transported lift of g (read on Bl_Z N for Z = g⁻¹Y) lies over g.

The induction

theorem AnalyticManifold.BlowUpSequence.eq_of_pullback_eq_of_step {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (hstep : ∀ {M U : AnalyticManifold 𝕜 E} (f g : AnalyticMap U M) {Y : Set M.carrier} {Z : Set U.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hZ : Manifold.IsClosedSubmanifold ψ₀ Z c), Manifold.IdealSheaf.pullback ⇑f ⋯ hY.idealSheaf = hZ.idealSheaf → Manifold.IdealSheaf.pullback ⇑g ⋯ hY.idealSheaf = hZ.idealSheaf → ∀ (J : U.IdealSheaf), Z ⊆ Manifold.IdealSheaf.support J → Hironaka.Manifold.AgreeOnSubspace f g J → ∀ (f' g' : AnalyticMap (Manifold.blowUp ψ₀ hZ) (Manifold.blowUp ψ₀ hY)), (∀ (q : (Manifold.blowUp ψ₀ hZ).carrier), (Manifold.blowUpπ ψ₀ hY) (f' q) = f ((Manifold.blowUpπ ψ₀ hZ) q)) → (∀ (q : (Manifold.blowUp ψ₀ hZ).carrier), (Manifold.blowUpπ ψ₀ hY) (g' q) = g ((Manifold.blowUpπ ψ₀ hZ) q)) → Hironaka.Manifold.AgreeOnSubspace f' g' (Manifold.MarkedIdealSheaf.birationalTransform hZ ⋯ { I := J, m := 1 }).I) (L : BlowUpSequence ψ₀ M) {U : AnalyticManifold 𝕜 E} (ψ ψ' : AnalyticMap U M) (hψ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ψ) (hψ' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ψ') (L' : BlowUpSequence ψ₀ M) (J : U.IdealSheaf) : Hironaka.Manifold.AgreeOnSubspace ψ ψ' J → (L.pullback ψ hψ).toSuccession.IsMarkedOne J → (∀ (i : Fin L.length), Manifold.IdealSheaf.support (L.toSuccession.center i) ⊆ Set.range ⇑(L.pullbackLift ψ hψ i.castSucc)) → (∀ (i : Fin L'.length), Manifold.IdealSheaf.support (L'.toSuccession.center i) ⊆ Set.range ⇑(L'.pullbackLift ψ' hψ' i.castSucc)) → L.pullback ψ hψ = L'.pullback ψ' hψ' → L = L'

The induction of Theorem 97 with the one-step lemma as a hypothesis (Kol07, Theorem 97, proof; [Wlo09, Lemma 5.5.3 (5)]). Let ψ, ψ' : U ⇉ M be local analytic isomorphisms agreeing on V(J), let L, L' be lists of centres of M with ψ^*L = ψ'^*L', the common pull-back of order ≥ 1 for (J, 1), and the centres of L, L' in the images of the lifts of ψ, ψ'. If (hstep) at every stage agreement on V(J_i) descends through the blow-up of a common centre Z ⊆ V(J_i) to agreement of the lifts on V((π_i)^{-1}_*(J_i, 1)), then L = L': at each stage the centre Z_i = ψ_i(Z_i^U) = ψ'_i(Z_i^U) = Z'_i, and the tails are compared over the blow-up of that centre.