The strict transforms along a succession are closed submanifolds

In Kollár's restriction of a blow-up sequence to a closed subscheme S, the stage S_{i+1}, the strict transform of S_i (the closure of π_i⁻¹(S_i ∖ Z_i)), is a closed subscheme of X_{i+1}, with natural embeddings S_i ↪ X_i [Kol07, Definition 30.2]. The one-step statement for manifolds is IsClosedSubmanifold.strictTransform (Transform/StrictCharts.lean, in the codimension-s form: the strict transform of a closed submanifold containing the centre is a closed submanifold, covered by the blow-up charts singled out in [Kol07, Theorem 88, proof]). Along a succession (FiniteSuccession.strictTransformSeq): every strict transform of a closed set is closed (isClosed_strictTransformSeq), the blow-downs carry S_{i+1} into S_i (strictTransformSeq_succ_subset_preimage), and under the hypothesis CentersIn every S_i is a closed submanifold of X_i of codimension s (isClosedSubmanifold_strictTransformSeq, by induction on the stage; the step's chosen chart chartAt i is exchanged for the given ψ through IsClosedSubmanifold.congr_chart). The strict transform of a closed subspace is described in [BM97, §3, Proposition 3.13].

theorem AnalyticManifold.FiniteSuccession.isClosed_strictTransformSeqAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) (hH : IsClosed H) (i : ℕ) (hi : i < S.length + 1) : IsClosed (S.strictTransformSeqAux H i hi)

The strict transforms of a closed set along the succession are closed.

theorem AnalyticManifold.FiniteSuccession.isClosed_strictTransformSeq {𝕜 : 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)) : IsClosed (S.strictTransformSeq H i)

The strict transforms of a closed set along the succession are closed.

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_succ_subset_preimage {𝕜 : 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) : S.strictTransformSeq H i.succ ⊆ ⇑(S.map i) ⁻¹' S.strictTransformSeq H i.castSucc

For closed H, the blow-down carries S_{i+1} into S_i (the maps π_i^S : S_{i+1} → S_i of a restricted blow-up sequence, [Kol07, Definition 30.2]).

theorem AnalyticManifold.FiniteSuccession.isClosedSubmanifold_strictTransformSeqAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length + 1) : Manifold.IsClosedSubmanifold ψ (S.strictTransformSeqAux H i hi) s

The strict transforms of a closed submanifold along the succession are closed submanifolds of the same codimension, at the level of the recursion.

theorem AnalyticManifold.FiniteSuccession.isClosedSubmanifold_strictTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin (S.length + 1)) : Manifold.IsClosedSubmanifold ψ (S.strictTransformSeq H i) s

Under the hypothesis Z_i ⊆ S_i for all i, every strict transform S_i is a closed submanifold of X_i of the codimension of S (the natural embeddings S_i ↪ X_i of [Kol07, Definition 30.2]).