Step 2.1 along an arbitrary local analytic isomorphism: preparatory lemmas

Kollár asks that a blow-up sequence functor commute with every smooth morphism, the value on a non-surjective one being the pull-back with its empty blow-ups deleted ([Kol07, 34.1], second bullet); the functoriality of Step 2.1 of the proof of [Kol07, Theorem 103] is that of Lemma 102 ([Kol07, 104, Step 2.3]). Along a local analytic isomorphism h : N → M that is not surjective a member E^j may become empty, so the iteration over the nonempty members of the pulled-back boundary runs over a sublist of the original one. This module proves the bookkeeping facts the induction over the members along h needs (Step21FamIndep.lean); they are not in the sources.

• BlowUpSequence.concat_nil_right — the empty sequence is a right unit for the concatenation (the contribution of a member emptied by h disappears);
• HypersurfaceFamily.nonemptyList_comap_eq_filter — the nonempty members of h⁻¹E in the order of the index set are the nonempty members of E whose preimage is nonempty (both lists are sorted without duplicates and have the same members);
• hyp_originalIdx_pullbackLiftLast_eq_empty — in the pull-back of the induced triple along the lift of h to the last stage, the member coming from an emptied E^j is empty (the strict transform of ∅ is ∅).

theorem AnalyticManifold.BlowUpSequence.concat_nil_right {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : L.concat (nil (L.stage (Fin.last L.length))) = L

The empty sequence of centres is a right unit for the concatenation.

theorem Manifold.HypersurfaceFamily.nonemptyList_comap_eq_filter {M N : Type u} (F : HypersurfaceFamily M) (h : N → M) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) (hF' : Finite { j : (comap h F).ι // (comap h F).hyp j ≠ ∅ }) : (comap h F).nonemptyList hF' = List.filter (fun (j : (comap h F).ι) => decide ((comap h F).hyp j ≠ ∅)) (F.nonemptyList hF)

The nonempty members of the pulled-back family, in the order of the index set, are the nonempty members of the family whose preimage is nonempty: both lists are sorted without duplicates and have the same members (a member with nonempty preimage is nonempty).

theorem Hironaka.Manifold.BO.hyp_originalIdx_pullbackLiftLast_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (j : F.ι) (hj : ⇑h ⁻¹' F.hyp j = ∅) : (Manifold.HypersurfaceFamily.comap (⇑(L.pullbackLiftLast h hh)) (L.toSuccession.totalTransformSeqFrom F (Fin.last L.toSuccession.length))).hyp (L.toSuccession.originalIdx F (Fin.last L.toSuccession.length) j) = ∅

In the pull-back along the lift to the last stage of the triple induced by a sequence L, the member coming from a member E^j with h⁻¹(E^j) = ∅ is empty: it is the strict transform of ∅ along the pulled-back sequence (strictTransformSeq_last_pullbackLiftLast, strictTransformSeq_empty).