Step 2.1 on an open: the cosupport misses the transforms of the members

At the end of Step 2.1 of the proof of [Kol07, Theorem 103], "cosupp(I_r, m) is disjoint from Π^{-1}_* E" (the conclusion of [Kol07, 104, Step 2.1.j] for every member i ≤ j). In the compatible-family form (Step21Fam.lean): at the end of Step 2.1 on a relatively compact open U, the cosupport of the controlled transform of 𝓘|_U misses the strict transform of every member of E|_U (step21FamOn_cosupp_disjoint). Along the chain:

• BlowUpSequence.disjoint_setOf_le_ord_strictTransformSeq_pullback, …_eraseEmpty — the clause "the cosupport of the last controlled transform misses the last strict transform of H" is carried along a pull-back (the last stage of the pulled-back sequence maps to the last stage by a local analytic isomorphism, markedTransformSeq_last_pullbackLiftLast, strictTransformSeq_last_pullbackLiftLast) and along the deletion of the empty blow-ups (markedTransformSeq_last_eraseEmpty, strictTransformSeq_last_eraseEmpty);
• ChainState.step21FamAux_cosupp_disjoint — along the chain, once a member has been processed the clause holds for it: Lemma 102 (1) of the family at that link (bd.cosupp_disjoint, the weak transform being the controlled one by bd.isOfOrder), pulled back to the link's open and carried through the concatenation (disjoint_concat_of_disjoint); the clauses of the members processed before persist along a sequence of order ≥ s (disjoint_setOf_le_ord_markedTransformSeq_strictTransformSeq);
• step21FamOn_cosupp_disjoint — the chain's clause restricted to U with the empty blow-ups deleted; an empty member has empty strict transform.

This is the clause of Step 2.1 that Step 2.2 in the compatible-family form needs (Step22Fam.lean).

theorem AnalyticManifold.BlowUpSequence.disjoint_setOf_le_ord_strictTransformSeq_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J E₀ : M.IdealSheaf) (m : ℕ) (hge : L.toSuccession.IsOfOrderGe J m E₀) (H : Set M.carrier) (hL : Disjoint {y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq J m (Fin.last L.toSuccession.length)) y} (L.toSuccession.strictTransformSeq H (Fin.last L.toSuccession.length))) : Disjoint {x : ↑↧((L.pullback h hh).toSuccession.stage (Fin.last (L.pullback h hh).toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((L.pullback h hh).toSuccession.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) m (Fin.last (L.pullback h hh).toSuccession.length)) x} ((L.pullback h hh).toSuccession.strictTransformSeq (⇑h ⁻¹' H) (Fin.last (L.pullback h hh).toSuccession.length))

The clause of Lemma 102 (1) pulls back (the local nature of [Kol07, 34.1]): if along L the cosupport of the last controlled transform of J misses the last strict transform of H, then along h^* L the cosupport of the last controlled transform of h^* J misses the last strict transform of h⁻¹(H). Both are read at the lift of the point to the last stage of L (markedTransformSeq_last_pullbackLiftLast, strictTransformSeq_last_pullbackLiftLast, ord_pullback_of_isLocalDiffeomorphAt).

theorem AnalyticManifold.BlowUpSequence.disjoint_setOf_le_ord_strictTransformSeq_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (J E₀ : M.IdealSheaf) (m : ℕ) (hge : L.toSuccession.IsOfOrderGe J m E₀) {H : Set M.carrier} (hH : IsClosed H) (hL : Disjoint {y : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq J m (Fin.last L.toSuccession.length)) y} (L.toSuccession.strictTransformSeq H (Fin.last L.toSuccession.length))) : Disjoint {x : ↑↧(L.eraseEmpty.toSuccession.stage (Fin.last L.eraseEmpty.toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord (L.eraseEmpty.toSuccession.markedTransformSeq J m (Fin.last L.eraseEmpty.toSuccession.length)) x} (L.eraseEmpty.toSuccession.strictTransformSeq H (Fin.last L.eraseEmpty.toSuccession.length))

The clause of Lemma 102 (1) survives the deletion of the empty blow-ups: the last stage of the cleaned sequence is the last stage of the sequence through the isomorphism eraseEmptyLast (markedTransformSeq_last_eraseEmpty, strictTransformSeq_last_eraseEmpty).

theorem Hironaka.Manifold.ChainState.step21FamAux_cosupp_disjoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (r : ℕ) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (l : List T.F.ι) (hl : l.length ≤ r) (j : T.F.ι) : j ∈ l → Disjoint {x : ↑↧((step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession.stage (Fin.last (step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession.markedTransformSeq (T.pullback (M.inclusion (W l.length)) ⋯).I s (Fin.last (step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession.length)) x} ((step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession.strictTransformSeq ((T.pullback (M.inclusion (W l.length)) ⋯).F.hyp j) (Fin.last (step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession.length))

Step 2.1 of the proof of [Kol07, Theorem 103] along the processed members, per open ([Kol07, 104, Step 2.1.j]: "Π^{-1}_{r(j)*}(E^i) ∩ cosupp(I_{r(j)}, m) = ∅ for i ≤ j"): after a member has been processed, the cosupport of the controlled transform misses its strict transform, at every later state of the chain. For the member processed last, this is Lemma 102 (1) of the family at that link (bd.cosupp_disjoint; its weak transform is the controlled one by bd.isOfOrder), read on the link's open through the lift of the restriction and carried through the concatenation (disjoint_concat_of_disjoint); for a member processed before, the clause at the previous state restricted to the smaller open persists along the appended sequence of order ≥ s (disjoint_setOf_le_ord_markedTransformSeq_strictTransformSeq).

theorem Hironaka.Manifold.step21FamOn_cosupp_disjoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (j : T.F.ι) : Disjoint {x : ↑↧((step21FamOn T s bd hT U hU).toSuccession.stage (Fin.last (step21FamOn T s bd hT U hU).toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord ((step21FamOn T s bd hT U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I s (Fin.last (step21FamOn T s bd hT U hU).toSuccession.length)) x} ((step21FamOn T s bd hT U hU).toSuccession.strictTransformSeq ((T.pullback (M.inclusion U) ⋯).F.hyp j) (Fin.last (step21FamOn T s bd hT U hU).toSuccession.length))

At the end of Step 2.1 the cosupport cosupp(I_r, m) "is disjoint from Π^{-1}_* E" (Step 2.1 of the proof of [Kol07, Theorem 103]; [Kol07, 104, Step 2.1.j]), per relatively compact open: at the end of Step 2.1 on U the cosupport of the controlled transform misses the strict transform of every member of E|_U. The chain's clause (step21FamAux_cosupp_disjoint) for a nonempty member, restricted to U with the empty blow-ups deleted; an empty member has empty strict transform.