Step 2.1 clears the boundary from the cosupport

After Step 2.1 of the proof of [Kol07, Theorem 103] has applied the functor of [Kol07, Lemma 102] to every nonempty member of E in the order of the index set, "cosupp(I_r, m) is disjoint from Π^{-1}_* E" ([Kol07, 104, Step 2.1.j]). Two facts carry the conclusion (1) of Lemma 102 for a member E^j through the later blow-ups: along a blow-up sequence of order ≥ m the cosupport {ord ≥ m} of the controlled transform lies over the cosupport of the ideal sheaf one started with (IsOfOrderGe.le_ord_stageMap), and the strict transform of a closed set lies over the set (strictTransform_subset_preimage, stage by stage). So a closed set missing the cosupport at the start has its strict transform missing the cosupport at every later stage (disjoint_setOf_le_ord_markedTransformSeq_strictTransformSeq). The concatenation of Step 2.1 transports the clause from the tail to the whole sequence (BlowUpSequence.disjoint_concat_of_disjoint), and the induction over the processed members (ChainState.step21FamAux_cosupp_disjoint, Step21FamCosupp.lean) uses Lemma 102 (1) for the member just processed and the two facts for the members processed before it. An empty member has empty strict transform (strictTransformSeq_empty).

• FiniteSuccession.strictTransformSeq_empty, FiniteSuccession.strictTransformSeq_subset_preimage_stageMap, FiniteSuccession.disjoint_setOf_le_ord_markedTransformSeq_strictTransformSeq — the two facts.
• BlowUpSequence.disjoint_concat_of_disjoint — the clause along a concatenation.

The clause for Step 2.1 in the compatible-family form, step21FamOn_cosupp_disjoint (Step21FamCosupp.lean), lets Step 2.2 run with the exceptional divisors and the transform of the hypersurface of maximal contact as its boundary while the sequence stays of order ≥ m for the full transformed boundary (Step22FamFull.lean).

theorem AnalyticManifold.FiniteSuccession.strictTransformSeqAux_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : ℕ) (hi : i < S.length + 1) : S.strictTransformSeqAux ∅ i hi = ∅

The strict transforms of the empty set are empty (in the form indexed by a natural number).

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin (S.length + 1)) : S.strictTransformSeq ∅ i = ∅

The strict transforms of the empty set are empty.

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_subset_preimage_stageMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} (hH : IsClosed H) (i : Fin (S.length + 1)) : S.strictTransformSeq H i ⊆ ⇑(S.stageMap i) ⁻¹' H

The strict transform of a closed set at stage i of a sequence lies over the set ([Kol07, Definition 25]): strictTransform_subset_preimage stage by stage.

theorem AnalyticManifold.FiniteSuccession.disjoint_setOf_le_ord_markedTransformSeq_strictTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) [FiniteDimensional 𝕜 E] {I E₀ : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe I m E₀) {H : Set M.carrier} (hH : IsClosed H) (hdis : Disjoint {x : ↑↧M.carrier | ↑m ≤ Manifold.IdealSheaf.ord I x} H) (i : Fin (S.length + 1)) : Disjoint {x : ↑↧(S.stage i).carrier | ↑m ≤ Manifold.IdealSheaf.ord (S.markedTransformSeq I m i) x} (S.strictTransformSeq H i)

Along a sequence of order ≥ m for (𝓘, m), a closed set missing the cosupport {ord 𝓘 ≥ m} has its strict transforms missing the cosupports of the controlled transforms: the cosupport at stage i lies over the cosupport at the start (IsOfOrderGe.le_ord_stageMap) and the strict transform over the set. This is how the conclusion of [Kol07, Lemma 102] for one member persists through the later blow-ups of Step 2.1 ([Kol07, 104, Step 2.1.j]).

theorem AnalyticManifold.BlowUpSequence.disjoint_concat_of_disjoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) (I : M.IdealSheaf) (m : ℕ) (H : Set M.carrier) : Disjoint {x : ↑↧(L'.toSuccession.stage (Fin.last L'.toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord (L'.toSuccession.markedTransformSeq (L.toSuccession.markedTransformSeq I m (Fin.last L.toSuccession.length)) m (Fin.last L'.toSuccession.length)) x} (L'.toSuccession.strictTransformSeq (L.toSuccession.strictTransformSeq H (Fin.last L.toSuccession.length)) (Fin.last L'.toSuccession.length)) → Disjoint {x : ↑↧((L.concat L').toSuccession.stage (Fin.last (L.concat L').toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((L.concat L').toSuccession.markedTransformSeq I m (Fin.last (L.concat L').toSuccession.length)) x} ((L.concat L').toSuccession.strictTransformSeq H (Fin.last (L.concat L').toSuccession.length))

The clause "the cosupport of the last controlled transform misses the last strict transform" along a concatenation L.concat L' follows from the clause along L' for the controlled transform and the strict transform reached by L; by induction on L, reading both sides through the first blow-up (cons_markedTransformSeqAux_succ, cons_strictTransformSeqAux_succ).