The two stop clauses along a push-forward from a hypersurface of maximal contact

Kollár's going-up theorem, [Kol07, Corollary 85], transports the order clause of a blow-up sequence on a hypersurface S of maximal contact to its push-forward (pushforward_isOfOrderGe_of_isOfOrderGe_traceFamily). The modified core of the modified first step is such a push-forward (the run of the functor one dimension down on the trace of the triple to H⁺, coreModOn), and the output clause and the stopped clause of ClauseTools.lean have to be transported the same way. This module is that transport, for a general push-forward FiniteSuccession.pushforward along a closed hypersurface S, given a hypersurface H of maximal contact (𝓘_H ≤ J) of which S is a clopen piece. The maximal contact of H⁺ itself fails where stopped components remain, so it is the maximal contact of H that is used, localised to S.

• isClosed_strictTransformSeq_diff (with strictTransformSeq_mono): a clopen piece S ⊆ H stays clopen in the strict transforms along a succession whose centres lie in the strict transforms of S (the strict transform of H at every stage is the strict transform of S together with the closed set of points over the stopped piece H ∖ S).
• eventually_stalkIdeal_idealSheaf_le_of_isClosed_diff: the maximal contact of the piece near each of its points, and at each point, from the global maximal contact of H (the hypotheses of restrict_maximalContact_of_stalkIdeal_le and of_restrict_maximalContact_of_eventually_le of StopRestrict.lean; off H both sides read J_x = ⊤).
• notMem_strictTransformSeq_of_stageMapAdd: a point off the strict transform stays off it along its fibre (strictTransformSeq_succ_subset_preimage); pushforwardIncl_stageMapAdd: the squares of the push-forward iterated along the composite blow-downs.
• support_totalTransformSeqFrom_traceFamily_eq_preimage: the support of the boundary of the lower run is the trace of the ambient boundary's (E_i ∩ S_i, [Kol07, Definition 30, 30.2]), through the identification at the level of reduced ideal sheaves (isSnc_totalTransformSeqFrom_and_boundarySeq_eq, boundarySeq_pushforwardStageIso, support_traceFamilyFrom_eq_support_boundarySeq).
• isSmoothTransversalIdealAt_pullback_pushforwardIncl, isSmoothTransversalIdealAt_of_pullback_pushforwardIncl: the predicate descends to and lifts from the lower stage, by the descent and lift of StopRestrict.lean at the strict transform of S, the stage isomorphism pushforwardStageIso, markedTransformSeq_pullback_pushforwardIncl for the ideal, and IsSmoothTransversalIdealAt.of_support_eq_nhds for the boundary.
• StoppedClause.pushforward: the stopped clause along the push-forward. A predicate point off the boundary is off the strict transform of S (no centre reaches its fibre), or of order 0 (notMem_center_of_ord_eq_zero), or the image of a lower predicate point, whose fibre the lower clause keeps off the lower centres.
• OutputClause.pushforward_of_mem_strictTransformSeq: the output clause along the push-forward at the points of the strict transform of S; the stopped piece is treated by OutputClause.pushforward in ClausePhaseBCore.lean.

The sources are [Kol07, Corollary 85], [Kol07, Definition 30, 30.2–30.3] and the modified first step of [Wlo09, Theorem 7.4.1]; the statements themselves are not in the sources.

theorem AnalyticManifold.FiniteSuccession.isClosed_strictTransformSeq_diff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S H : Set M.carrier} (hSc : IsClosed S) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) (hc : B.CentersIn S) (i : Fin (B.length + 1)) : IsClosed (B.strictTransformSeq H i \ B.strictTransformSeq S i)

A clopen piece stays clopen along a succession with centres inside it: for S ⊆ H closed with H \ S closed and every centre inside the strict transform of S, the strict transform of H at every stage is the strict transform of S together with the (closed) preimage of H \ S, disjoint from it. The strict transform of a union is the union, and that of a set the centre misses is its preimage (strictTransformSeq_succ, strictTransformSeq_succ_subset_preimage, strictTransformSeq_mono).

theorem AnalyticManifold.FiniteSuccession.eventually_stalkIdeal_idealSheaf_le_of_isClosed_diff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S H : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (hH : Manifold.IsClosedSubmanifold ψ H 1) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) {J : M.IdealSheaf} (hle : hH.idealSheaf ≤ J) {y : M.carrier} (hy : y ∈ S) : ∀ᶠ (x : ↑↧M.carrier) in nhds y, hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal J x

The maximal contact of the clopen piece near each of its points: for S ⊆ H closed hypersurfaces with H \ S closed and 𝓘_H ≤ J, at every point y ∈ S the stalks of 𝓘_S and 𝓘_H agree on the open (H \ S)ᶜ ∋ y (the vanishing ideal depends on the germ of the set, vanishingStalk_inter_of_mem_nhds), and off H both read J_x = ⊤; so 𝓘_S ≤ J holds stalkwise on a neighbourhood of y, which is the hypothesis of of_restrict_maximalContact_of_eventually_le, and at y that of restrict_maximalContact_of_stalkIdeal_le.

theorem AnalyticManifold.FiniteSuccession.notMem_strictTransformSeq_of_stageMapAdd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S : Set M.carrier} (hSc : IsClosed S) (i k : ℕ) (h : i + k < B.length + 1) {x : (B.stage ⟨i, ⋯⟩).carrier} (hx : x ∉ B.strictTransformSeq S ⟨i, ⋯⟩) (y : (B.stage ⟨i + k, h⟩).carrier) (hy : (B.stageMapAdd i k h) y = x) : y ∉ B.strictTransformSeq S ⟨i + k, h⟩

A point off the strict transform stays off it along its fibre: the strict transform of a closed set at a stage lies in the preimage of the strict transform at the stage before (strictTransformSeq_succ_subset_preimage), iterated along stageMapAdd.

theorem AnalyticManifold.FiniteSuccession.pushforwardIncl_stageMapAdd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) (i k : ℕ) (h : i + k < T.length + 1) (y : (T.stage ⟨i + k, h⟩).carrier) : (pushforwardIncl hS T ⟨i, ⋯⟩) ((T.stageMapAdd i k h) y) = ((pushforward hS T).stageMapAdd i k h) ((pushforwardIncl hS T ⟨i + k, h⟩) y)

The inclusions of the stages commute with the composite blow-downs (the squares pushforwardIncl_map iterated along stageMapAdd).

theorem AnalyticManifold.FiniteSuccession.exists_diffeomorph_inclusionMap_pushforwardIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin (T.length + 1)) (hSi : Manifold.IsClosedSubmanifold ψ ((pushforward hS T).strictTransformSeq S i) 1) : ∃ (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (T.stage i).carrier hSi.toAnalyticManifold.carrier ⊤), ∀ (x' : (T.stage i).carrier), hSi.inclusionMap (e x') = (pushforwardIncl hS T i) x'

The stage of the lower sequence is diffeomorphic to the bundled strict transform of S through the inclusion of the stage (pushforwardStageIso, carried across the identity of sets range (pushforwardIncl i) = strictTransformSeq S i by IsClosedSubmanifold.diffeomorphOfEq).

theorem AnalyticManifold.FiniteSuccession.support_totalTransformSeqFrom_traceFamily_eq_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {J : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord J y ≤ 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 (hS.traceFamily F).idealSheaf) (i : Fin (T.length + 1)) : (T.totalTransformSeqFrom (hS.traceFamily F) i).support = ⇑(pushforwardIncl hS T i) ⁻¹' ((pushforward hS T).totalTransformSeqFrom F i).support

The support of the boundary of the lower run is the trace of the ambient boundary's (the E_i ∩ S_i of [Kol07, Definition 30, 30.2] at the level of supports): the lower boundary's support is that of its reduced ideal sheaf (isSnc_totalTransformSeqFrom_and_boundarySeq_eq), which pulls back along the stage isomorphism from the boundary of Π|_S (boundarySeq_pushforwardStageIso), whose support is the trace of the ambient boundary's (support_traceFamilyFrom_eq_support_boundarySeq, support_traceFamilyFrom).

theorem AnalyticManifold.FiniteSuccession.isSmoothTransversalIdealAt_pullback_pushforwardIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {J : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord J y ≤ 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 (hS.traceFamily F).idealSheaf) (i : Fin (T.length + 1)) {x' : (T.stage i).carrier} (hSi : Manifold.IsClosedSubmanifold ψ ((pushforward hS T).strictTransformSeq S i) 1) (hle : hSi.idealSheaf.stalkIdeal ((pushforwardIncl hS T i) x') ≤ Manifold.IdealSheaf.stalkIdeal ((pushforward hS T).markedTransformSeq J 1 i) ((pushforwardIncl hS T i) x')) (hJ : Manifold.IdealSheaf.stalkIdeal ((pushforward hS T).markedTransformSeq J 1 i) ((pushforwardIncl hS T i) x') ≠ ⊤) (h : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ ((pushforward hS T).totalTransformSeqFrom F i) ((pushforward hS T).markedTransformSeq J 1 i) ((pushforwardIncl hS T i) x')) : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (T.totalTransformSeqFrom (hS.traceFamily F) i) (T.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 i) x'

The predicate descends from the ambient stage to the lower stage: restrict_maximalContact_of_stalkIdeal_le on the ambient stage at the strict transform S_i, with the maximal contact at the point hle, transported along the stage isomorphism pushforwardStageIso (IsSmoothTransversalIdealAt.comap, restrictIncl_pushforwardStageIso); the ideal is the lower marked transform by markedTransformSeq_pullback_pushforwardIncl; the boundary by IsSmoothTransversalIdealAt.of_support_eq_nhds with support_totalTransformSeqFrom_traceFamily_eq_preimage, both families having simple normal crossings (isSnc_traceFamilyFrom, isSnc_comap, isSnc_totalTransformSeqFrom_and_boundarySeq_eq).

theorem AnalyticManifold.FiniteSuccession.isSmoothTransversalIdealAt_of_pullback_pushforwardIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {J : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord J y ≤ 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 (hS.traceFamily F).idealSheaf) (i : Fin (T.length + 1)) {x' : (T.stage i).carrier} (hSi : Manifold.IsClosedSubmanifold ψ ((pushforward hS T).strictTransformSeq S i) 1) (hle : ∀ᶠ (x : ↑↧((pushforward hS T).stage i).carrier) in nhds ((pushforwardIncl hS T i) x'), hSi.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal ((pushforward hS T).markedTransformSeq J 1 i) x) (hJ : Manifold.IdealSheaf.stalkIdeal ((pushforward hS T).markedTransformSeq J 1 i) ((pushforwardIncl hS T i) x') ≠ ⊤) (h : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (T.totalTransformSeqFrom (hS.traceFamily F) i) (T.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 i) x') : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ ((pushforward hS T).totalTransformSeqFrom F i) ((pushforward hS T).markedTransformSeq J 1 i) ((pushforwardIncl hS T i) x')

The predicate lifts from the lower stage to the ambient stage (the converse of isSmoothTransversalIdealAt_pullback_pushforwardIncl, for the output clause): the lower predicate transported to the trace family (the stage isomorphism, IsSmoothTransversalIdealAt.of_support_eq_nhds with support_totalTransformSeqFrom_traceFamily_eq_preimage), then of_restrict_maximalContact_of_eventually_le with the ambient boundary in proper normal crossings with S_i (hasSncWithProper_totalTransformSeqFrom_strictTransformSeq_of_forall_lt) and the maximal contact on a neighbourhood.

theorem AnalyticManifold.FiniteSuccession.StoppedClause.pushforward {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {J : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} {H : Set M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord J y ≤ 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 (hS.traceFamily F).idealSheaf) (hH : Manifold.IsClosedSubmanifold ψ H 1) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) (hle : hH.idealSheaf ≤ J) (hP : StoppedClause (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) T (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) (hS.traceFamily F)) : StoppedClause ψ (FiniteSuccession.pushforward hS T) J F

The stopped clause along a push-forward ([Kol07, Corollary 85] for the stopped clause): the push-forward of a sequence with the stopped clause for the trace triple has the stopped clause, given a hypersurface H of maximal contact (𝓘_H ≤ J) of which S is a clopen piece. At a predicate point x of a stage off the boundary: if x ∉ S_i, no centre reaches its fibre (notMem_strictTransformSeq_of_stageMapAdd, centersIn_pushforward); if x = incl x' and ord 𝓘_i x = 0, no centre reaches its fibre (notMem_center_of_ord_eq_zero); otherwise the maximal contact of S_i at x (from that of H, isClosed_strictTransformSeq_diff, eventually_stalkIdeal_idealSheaf_le_of_isClosed_diff) lets isSmoothTransversalIdealAt_pullback_pushforwardIncl descend the predicate to x', off the lower boundary (support_totalTransformSeqFrom_traceFamily_eq_preimage), the lower clause keeps its fibre off the lower centres, and a point of the ambient fibre is either off S_{i+k} (no centre) or the image of a lower fibre point (pushforwardIncl_stageMapAdd, the injectivity of the inclusions, support_center_pushforward).

theorem AnalyticManifold.FiniteSuccession.OutputClause.pushforward_of_mem_strictTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (T : hS.toAnalyticManifold.FiniteSuccession) {J : M.IdealSheaf} {F : Manifold.HypersurfaceFamily M.carrier} {H : Set M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord J y ≤ 1) (hT : T.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) 1 (hS.traceFamily F).idealSheaf) (hH : Manifold.IsClosedSubmanifold ψ H 1) (hSH : S ⊆ H) (hcl : IsClosed (H \ S)) (hle : hH.idealSheaf ≤ J) (hO : OutputClause (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) T (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J) (hS.traceFamily F)) {x : ((FiniteSuccession.pushforward hS T).stage (Fin.last (FiniteSuccession.pushforward hS T).length)).carrier} (hx : x ∈ (FiniteSuccession.pushforward hS T).strictTransformSeq S (Fin.last (FiniteSuccession.pushforward hS T).length)) (hord : 1 ≤ Manifold.IdealSheaf.ord ((FiniteSuccession.pushforward hS T).markedTransformSeq J 1 (Fin.last (FiniteSuccession.pushforward hS T).length)) x) : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ ((FiniteSuccession.pushforward hS T).totalTransformSeqFrom F (Fin.last (FiniteSuccession.pushforward hS T).length)) ((FiniteSuccession.pushforward hS T).markedTransformSeq J 1 (Fin.last (FiniteSuccession.pushforward hS T).length)) x

The output clause along a push-forward, at the points of the strict transform of S ([Kol07, Corollary 85] for the output clause; the stopped piece H_last \ S_last is treated by OutputClause.pushforward in ClausePhaseBCore.lean): at a support point x = incl x' of the last stage the lower marked transform has order ≥ 1 at x' (ord_le_ord_pullback through markedTransformSeq_pullback_pushforwardIncl), the lower clause gives the predicate at x', and isSmoothTransversalIdealAt_of_pullback_pushforwardIncl lifts it with the maximal contact on a neighbourhood (eventually_stalkIdeal_idealSheaf_le_of_isClosed_diff).