Padding the disjoining list by empty blow-ups

Kollár's empty-blow-up convention [Kol07, 32] for the disjoining list: when the (m+2)-fold locus of E is already empty, the first round of disjoinList (m+2) blows up the empty centre and the rest is the pull-back of disjoinList (m+1) along the blow-down Bl_∅ M → M (the strict transform along an empty blow-up is the preimage, strictTransformSet_empty_of_isClosed). The value built from the padded list is the value built from the unpadded one:

• the empty first round is erased (eraseEmpty_cons_of_eq_empty) and its blow-down carried through the shrink-and-append step (shrinkAppend_pullback_eraseEmpty, with the compatibility of the input family on the two reading opens) — valueOf_cons_of_eq_empty;
• the pulled-back list is compared with the list itself by valueOf_pullback, the disjoined triple of the padded list being an empty extension of the pull-back of the disjoined triple (isEmptyExtensionOfPullback_disjoinedTripleOf_cons_of_eq_empty) — the padded exceptional divisor is empty and the input family is indifferent to it.

Iterating, the value built from disjoinList k for the disjoined triple does not depend on the admissible bound k (valueOf_disjoinList_eq) — the first half of the canonicity of the shrinking chain (the disjoining bounds over two shrinking opens differ), completed in Canonicity.lean. This realises Kollár's functoriality for smooth morphisms [Kol07, 34.1], where a pull-back is compared with the value "by deleting every blow-up whose center is empty".

The padded disjoining list

theorem Hironaka.Manifold.disjoinList_succ_succ_eq_cons_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) {m : ℕ} (hm₂ : F.meetLocus (m + 2 + 1) = ∅) (hm₁ : F.meetLocus (m + 2) = ∅) : disjoinList (m + 2) F hF hm₂ = AnalyticManifold.BlowUpSequence.cons ⋯ ((disjoinList (m + 1) F hF hm₁).pullback (Manifold.blowUpπ ψ₀ ⋯) ⋯)

The empty-blow-up convention [Kol07, 32] for the disjoining list: when the (m+2)-fold locus is already empty, the first round of disjoinList (m+2) blows up the empty centre and the rest is the pull-back of disjoinList (m+1) along the blow-down.

theorem Hironaka.Manifold.isSnc_totalTransformSeqFrom_last_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (e : L₁ = L₂) (F : Manifold.HypersurfaceFamily M.carrier) (h : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L₁.toSuccession.totalTransformSeqFrom F (Fin.last L₁.toSuccession.length))) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L₂.toSuccession.totalTransformSeqFrom F (Fin.last L₂.toSuccession.length))

Transport of the snc hypothesis on the boundary along an equality of lists.

theorem Hironaka.Manifold.meetLocus_two_subfamily_original_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (e : L₁ = L₂) (F : Manifold.HypersurfaceFamily M.carrier) (h : ((L₁.toSuccession.totalTransformSeqFrom F (Fin.last L₁.toSuccession.length)).subfamily fun (k : (L₁.toSuccession.totalTransformSeqFrom F (Fin.last L₁.toSuccession.length)).ι) => k ∈ Set.range (L₁.toSuccession.originalIdx F (Fin.last L₁.toSuccession.length))).meetLocus 2 = ∅) : ((L₂.toSuccession.totalTransformSeqFrom F (Fin.last L₂.toSuccession.length)).subfamily fun (k : (L₂.toSuccession.totalTransformSeqFrom F (Fin.last L₂.toSuccession.length)).ι) => k ∈ Set.range (L₂.toSuccession.originalIdx F (Fin.last L₂.toSuccession.length))).meetLocus 2 = ∅

Transport of the disjointness hypothesis on the original members along an equality of lists.

theorem Hironaka.Manifold.isCompact_closure_range_of_comp_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A B N : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤) (ι₁ : AnalyticMap N A) (ι : AnalyticMap N B) (h : ∀ (p : N.carrier), φ (ι₁ p) = ι p) (hc : IsCompact (closure (Set.range ⇑ι))) : IsCompact (closure (Set.range ⇑ι₁))

A map with relatively compact range, composed with an analytic isomorphism: the range of the other factor is relatively compact.

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_cons_shrinkAppend_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X N : AnalyticManifold 𝕜 E} {Y : Set X.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (R : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ι) (hY₀' : ⇑ι ⁻¹' Y = ∅) (B : BlowUpSequence ψ₀ ((R.stage (Fin.last R.length)).restrict (R.liftRange (liftStep ι hι hY) ⋯))) (ι₁ : AnalyticMap N (Manifold.blowUp ψ₀ hY)) (hι₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ι₁) (hcomp : ContMDiffMap.comp (liftStep ι hι hY) (emptyBlowUpDiffeomorph ⋯ hY₀').symm.toAnalyticMap = ι₁) (B₁ : BlowUpSequence ψ₀ ((R.stage (Fin.last R.length)).restrict (R.liftRange ι₁ hι₁))) (hle : R.liftRange ι₁ hι₁ ≤ R.liftRange (liftStep ι hι hY) ⋯) (hB : B₁.eraseEmpty = (B.pullback ((R.stage (Fin.last R.length)).restrictLE hle) ⋯).eraseEmpty) : ((cons hY R).shrinkAppend ι hι B).eraseEmpty = (R.shrinkAppend ι₁ hι₁ B₁).eraseEmpty

The shrink-and-append step of a list whose first round is empty over the reading map: the empty round is erased and its blow-down carried through the step along the corestricted lift (eraseEmpty_cons_of_eq_empty, shrinkAppend_pullback_eraseEmpty).

The value of a list whose first round is empty

theorem Hironaka.Manifold.valueOf_cons_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {Y : Set X.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Y c) (R : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY)) (T₂ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((AnalyticManifold.BlowUpSequence.cons hY R).stage (Fin.last (AnalyticManifold.BlowUpSequence.cons hY R).length))) (hT₂ : Manifold.AnalyticTriple.BMOClass 1 T₂) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) (hY₀' : ⇑ι ⁻¹' Y = ∅) (ι₁ : AnalyticMap N (Manifold.blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY)) (hι₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι₁) (hc₁ : IsCompact (closure (Set.range ⇑ι₁))) (hcomp : ContMDiffMap.comp (AnalyticManifold.BlowUpSequence.liftStep ι hι hY) (AnalyticManifold.BlowUpSequence.emptyBlowUpDiffeomorph ⋯ hY₀').symm.toAnalyticMap = ι₁) : valueOf bmo (AnalyticManifold.BlowUpSequence.cons hY R) T₂ hT₂ ι hι hc = valueOf bmo R T₂ hT₂ ι₁ hι₁ hc₁

The value built from a list whose first centre is empty over the reading map ι is the value built from its tail, read along the lift of ι composed with the inverse of the empty blow-up.

One padding step

theorem Hironaka.Manifold.valueOf_disjoinedTripleOf_cons_pullback_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) {Y : Set X.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Y c) (hY₀ : Y = ∅) (h₁ : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length))) (h₁' : ((L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).subfamily fun (k : (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).ι) => k ∈ Set.range (L.toSuccession.originalIdx T.F (Fin.last L.toSuccession.length))).meetLocus 2 = ∅) (h₂ : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.totalTransformSeqFrom T.F (Fin.last (AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.length))) (h₂' : (((AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.totalTransformSeqFrom T.F (Fin.last (AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.length)).subfamily fun (k : ((AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.totalTransformSeqFrom T.F (Fin.last (AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.length)).ι) => k ∈ Set.range ((AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.originalIdx T.F (Fin.last (AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)).toSuccession.length))).meetLocus 2 = ∅) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) : valueOf bmo (AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)) (disjoinedTripleOf T (AnalyticManifold.BlowUpSequence.cons hY (L.pullback (Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) hY) ⋯)) h₂ h₂') ⋯ ι hι hc = valueOf bmo L (disjoinedTripleOf T L h₁ h₁') ⋯ ι hι hc

The empty-blow-up convention [Kol07, 32] for the value: the value built from the list padded by an empty first round, cons h∅ (π^* L), and its disjoined triple is the value built from L and its disjoined triple.

Independence of the disjoining bound

theorem Hironaka.Manifold.valueOf_disjoinList_succ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) (k : ℕ) (hk : T.F.meetLocus (k + 1) = ∅) (hk' : T.F.meetLocus (k + 1 + 1) = ∅) : valueOf bmo (disjoinList (k + 1) T.F ⋯ hk') (disjoinedTriple T hk') ⋯ ι hι hc = valueOf bmo (disjoinList k T.F ⋯ hk) (disjoinedTriple T hk) ⋯ ι hι hc

One padding step for the disjoining list of a triple: the value at the bound k + 1 is the value at the bound k (both admissible).

theorem Hironaka.Manifold.valueOf_disjoinList_add {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) (d k : ℕ) (hk : T.F.meetLocus (k + 1) = ∅) (hkd : T.F.meetLocus (k + d + 1) = ∅) : valueOf bmo (disjoinList (k + d) T.F ⋯ hkd) (disjoinedTriple T hkd) ⋯ ι hι hc = valueOf bmo (disjoinList k T.F ⋯ hk) (disjoinedTriple T hk) ⋯ ι hι hc

Iterated padding: the value at the bound k + d is the value at the bound k.

theorem Hironaka.Manifold.valueOf_disjoinList_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo : BMOanFam 𝕜 n 1) {X N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hc : IsCompact (closure (Set.range ⇑ι))) (k₁ k₂ : ℕ) (hk₁ : T.F.meetLocus (k₁ + 1) = ∅) (hk₂ : T.F.meetLocus (k₂ + 1) = ∅) : valueOf bmo (disjoinList k₁ T.F ⋯ hk₁) (disjoinedTriple T hk₁) ⋯ ι hι hc = valueOf bmo (disjoinList k₂ T.F ⋯ hk₂) (disjoinedTriple T hk₂) ⋯ ι hι hc

The value does not depend on the admissible disjoining bound ([Kol07, 32]): for two bounds k₁, k₂ with E having no (kᵢ+1)-fold points, the values built from disjoinList k₁ and disjoinList k₂ with their disjoined triples agree.