The boundary of a push-forward traces to the boundary of the given sequence

Kollár pushes a blow-up sequence T of a closed submanifold S ⊆ M forward to a sequence Π = j_* T of M with the same centres, and reads the boundary of Π back on the carried strict transforms S_i through the inclusions j_i : T_i → X_i [Kol07, Definitions 30.2–30.3]. BoundaryTrace.lean provides the invariant that the boundary family F_i^X of Π has simple normal crossings with S_i PROPERLY (hasSncWithProper_totalTransformSeq_strictTransformSeq_of_forall_lt) and the UNION-level identification of its trace with the boundary of Π|_S (traceFamily; boundarySeq_pushforwardStageIso of GoingUp/StageIso.lean). The gluing of the exceptional families along the padding needs the MEMBER-level trace identity — which exceptional divisor of Π traces to which of T — and the ideal-theoretic form of the trace of a transverse member. This file proves both, with no blow-up-chart computation on the slice: the proper simple-normal-crossings chart of the AMBIENT stage and a one-coordinate density argument suffice.

• preimage_pushforwardIncl_preimage_center, preimage_pushforwardIncl_preimage_diff_center, preimage_pushforwardIncl_strictTransformSet: the three steps of the induction.
• exists_orderIso_totalTransformSeq_pushforward: the trace identity at every stage — an order isomorphism of the index types with j_i⁻¹(H^X_{i, o j}) = H_{i, j}.
• IsClosedSubmanifold.pullback_idealSheaf_inclusionMap_of_hasSncWithProper: the ideal sheaf of a member pulled back along the inclusion of a closed submanifold having simple normal crossings with the family properly is the ideal sheaf of its trace.

Used by LocalResolutionPad.lean (exists_closedSubmanifold_last_pushforwardRestrict_boundary) and PushforwardFamily.lean. Not in the sources; routine.

theorem AnalyticManifold.FiniteSuccession.preimage_pushforwardIncl_preimage_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin T.length) : ⇑(pushforwardIncl hS T i.succ) ⁻¹' ⇑((pushforward hS T).map i) ⁻¹' Manifold.IdealSheaf.support ((pushforward hS T).center i) = ⇑(T.map i) ⁻¹' Manifold.IdealSheaf.support (T.center i)

The NEW member: the exceptional divisor of the push-forward's step traces on the slice to the exceptional divisor of the given step ([Kol07, Definition 30.3]): j_{i+1}⁻¹(π⁻¹ Z^X) = π_T⁻¹ Z — the square pushforwardIncl_map, the centre Z^X = j_i(Z) (support_center_pushforward) and the injectivity of j_i.

theorem AnalyticManifold.FiniteSuccession.preimage_pushforwardIncl_preimage_diff_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin T.length) {A : Set ((pushforward hS T).stage i.castSucc).carrier} {B : Set (T.stage i.castSucc).carrier} (hAB : ⇑(pushforwardIncl hS T i.castSucc) ⁻¹' A = B) : ⇑(pushforwardIncl hS T i.succ) ⁻¹' ⇑((pushforward hS T).map i) ⁻¹' (A \ Manifold.IdealSheaf.support ((pushforward hS T).center i)) = ⇑(T.map i) ⁻¹' (B \ Manifold.IdealSheaf.support (T.center i))

The part of a member off the centre traces to the part of its trace off the centre: j_{i+1}⁻¹(π⁻¹(A ∖ Z^X)) = π_T⁻¹(B ∖ Z) when j_i⁻¹ A = B.

theorem AnalyticManifold.FiniteSuccession.preimage_pushforwardIncl_strictTransformSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin T.length) (hsnc₀ : Manifold.HypersurfaceFamily.IsSnc ψ ((pushforward hS T).totalTransformSeq i.castSucc)) (hprop : Manifold.HypersurfaceFamily.HasSncWithProper ψ ((pushforward hS T).totalTransformSeq i.succ) ((pushforward hS T).strictTransformSeq S i.succ) s) (k₀ : ((pushforward hS T).totalTransformSeq i.castSucc).ι) {B : Set (T.stage i.castSucc).carrier} (hAB : ⇑(pushforwardIncl hS T i.castSucc) ⁻¹' ((pushforward hS T).totalTransformSeq i.castSucc).hyp k₀ = B) : ⇑(pushforwardIncl hS T i.succ) ⁻¹' Manifold.strictTransformSet (⇑((pushforward hS T).map i)) (Manifold.IdealSheaf.support ((pushforward hS T).center i)) (((pushforward hS T).totalTransformSeq i.castSucc).hyp k₀) = Manifold.strictTransformSet (⇑(T.map i)) (Manifold.IdealSheaf.support (T.center i)) B

An OLD member ([Kol07, Definition 30.2]): the strict transform commutes with the trace on the carried slice — for a member A of the push-forward's boundary at stage i whose trace on T_i is B, the trace on T_{i+1} of the strict transform of A is the strict transform of B. ⊇ by continuity of j_{i+1} and preimage_pushforwardIncl_preimage_diff_center. ⊆: at x = j_{i+1} q' on the strict transform of A, if x is off the exceptional divisor E' then x ∈ π⁻¹(A ∖ Z^X) itself; if x ∈ E', the proper simple-normal-crossings chart of the boundary at x along S_{i+1} (hasSncWithProper_totalTransform) has the member as {y_c = 0} and E' as {y_d = 0}, c ≠ d, both off the S_{i+1}-block; moving the d-coordinate alone, y_t := φ⁻¹(ψ⁻¹(update (ψ (φ x)) d t)), t ≠ 0, lies on S_{i+1} and on the member and off E', so in π⁻¹(A ∖ Z^X) ∩ S_{i+1}, and y_t → x — x is in the closure, and q' is in the closure of the trace by IsInducing.closure_eq_preimage_closure_image.

theorem AnalyticManifold.FiniteSuccession.exists_orderIso_totalTransformSeq_pushforward {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (h3 : ∀ (i : Fin T.length), ((pushforward hS T).boundarySeq ⊤ i.castSucc).HasOnlyNormalCrossingsWith ((pushforward hS T).center i)) (i : Fin (T.length + 1)) : ∃ (o : (T.totalTransformSeq i).ι ≃o ((pushforward hS T).totalTransformSeq i).ι), ∀ (j : (T.totalTransformSeq i).ι), ⇑(pushforwardIncl hS T i) ⁻¹' ((pushforward hS T).totalTransformSeq i).hyp (o j) = (T.totalTransformSeq i).hyp j

The boundary family of the push-forward traces, member by member and in order, to the boundary family of the given sequence ([Kol07, Definitions 30.2–30.3]): an order isomorphism o of the last-stage index types (OrderIso.sumLexCongr on the ⊕ₗ PUnit towers) with j_i⁻¹(H^X_{i, o j}) = H_{i, j} at every stage, under the normal-crossings clause (3′) of [Kol07, Definition 66] for the push-forward (the input of hasSncWithProper_totalTransformSeq_strictTransformSeq in its prefix-bounded form). Induction on the stage: the new member by preimage_pushforwardIncl_preimage_center, an old member by preimage_pushforwardIncl_strictTransformSet.

theorem Manifold.IsClosedSubmanifold.pullback_idealSheaf_inclusionMap_of_hasSncWithProper {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {F : HypersurfaceFamily M.carrier} (hF : HypersurfaceFamily.IsSnc ψ F) (hFS : HypersurfaceFamily.HasSncWithProper ψ F S s) (j : F.ι) : IdealSheaf.pullback ⇑hS.inclusionMap ⋯ ⋯.idealSheaf = ⋯.idealSheaf

The ideal sheaf of a member of a family having simple normal crossings with the closed submanifold S PROPERLY, pulled back along the inclusion of S, is the ideal sheaf of its trace (the boundary E_i ∩ S_i of [Kol07, Definition 30.2] at the level of ideals) — the counterpart of idealSheaf_preimageVal_eq_pullback (GermRestrict.lean) for a TRANSVERSE hypersurface. Stalkwise: on the trace, the member is {y_c = 0} in the proper chart with c off the S-block (ker_restrictStalk_eq_span at the singleEmb adapted chart), the trace is {y_c|_S = 0} in the induced chart (isSncChartAt_inducedChart), and the coordinate germ y_c restricts along the inclusion to the induced coordinate (germMap_germ, germ_ext); off the trace both stalks are the unit ideal.