The stop predicate on a hypersurface of maximal contact: descent and lift

The modified marked resolution recurses on the dimension inside its first step ([Wlo09, Theorem 7.4.1]): the functor one dimension down runs on the restriction of the ideal to the hypersurface of maximal contact H⁺ and its centres are pushed forward. The two clauses of the structure BMOmodFam about the stop predicate IsSmoothTransversalIdealAt therefore have to move between the ambient manifold and H, as in Włodarczyk's argument for the strict transforms ([Wlo05, Theorem 4.7.1, proof]: the predicate for (F, J) at a point y ∈ H descends to the trace family and the restricted ideal on H, and the predicate on H lifts back because u ∈ J for the equation u of H, "since u ∈ σ^c(I) it follows that σ^c(I) = I_{Ỹ₁}"). This module proves the two directions and the chart facts they share; the persistence half is StopPersistence.lean.

• Chart facts. exists_chart_of_linearIndependent_linearPart: n sections near y, vanishing at y, whose linear parts in one chart of the maximal atlas are linearly independent, are the coordinates (up to a permutation of the indices) of a chart of the maximal atlas at y (exists_chart_extending read through the linear parts of Chart/Cotangent.lean). exists_eq_sum_of_germ_mem_span: a germ in the ideal spanned by finitely many germs is, on a neighbourhood, a combination of their representatives with section coefficients. IsClosedSubmanifold.restrictStalk_coord_eq_coord_chartOn: the restriction to a closed submanifold of a coordinate germ off the block of an adapted chart is the corresponding coordinate germ of the induced chart. IsSncChartAt.frequently_notMem_of_notMem_range: in a chart adapted to H which is a chart with simple normal crossings for F, a member whose coordinate is off the block of H does not contain H near the point.
• Descent. IsSmoothTransversalIdealAt.restrict_maximalContact: for H of maximal contact at the mark 1 (𝓘_H ≤ J), y ∈ H in the cosupport of J, and the predicate for (F, J) at y, the predicate holds on the bundled H for the trace family and J|_H. The equation u of H lies in J_y = (z_σ) and not in 𝔪_y², so a coefficient a_{i₀} is a unit near y (linearPart_mul_of_mem_maximalIdeal) and u replaces the coordinate z_{σ i₀} (exists_chart_of_linearIndependent_linearPart with linearIndependent_update_tilt); in the new chart the members through y stay coordinate hyperplanes, H = {u = 0}, and J = (u, z_{σ i}, i ≠ i₀) (exists_eq_sum_of_germ_mem_span); the induced chart of H is a chart with simple normal crossings for the trace family (IsSncChartAt.restrict_isSncChartAt, frequently_notMem_of_notMem_range) on which J|_H is spanned by the c − 1 restricted coordinates (stalkIdeal_pullback, germMap_inclusionMap, restrictStalk_coord_eq_coord_chartOn, restrictStalk_coord_sub).
• Lift. IsSmoothTransversalIdealAt.of_restrict_maximalContact: for H of maximal contact with F ∪ H of simple normal crossings and the members not containing H (HasSncWithProper), y ∈ H in the cosupport of J, and the predicate on H for the trace family and J|_H, the predicate holds for (F, J) at y. An adapted chart φₐ of H which is a chart with simple normal crossings for F gives the retraction r onto H along the u-direction (the inverse of the induced chart after the projection off the block); the new ambient coordinates are u and the cylinder extensions w_m ∘ r of the coordinates of the chart of the hypersurface, independent because the linear parts of the w_m in the induced chart form a basis (linearIndependent_cotangentClass_iff_linearPart) and u is transverse. In the chart φₐ the members are cylinders over their traces, so they are coordinate hyperplanes of the new chart; H = {u = 0}; at a ∈ H the ideal is J_a = (u) + (J|_H)_a lifted (ker_restrictStalk_eq_span, Ideal.comap_map_of_surjective, restrictStalk_surjective), and off H it is the unit ideal.

The identification of the transforms and centres of the pushed-forward run with those of the run one dimension down is markedTransformSeq_pullback_pushforwardIncl, support_center_pushforward and noEmptyCenters_pushforwardRestrict, which ClausePushforward.lean and ClauseClosedEmbedding.lean use on the way to the two clauses; BlowUpSequence.toSuccession_pushforward and pushforwardRestrictOf_eq are the forms used by the closed-embedding functor (ClosedEmbeddingFam.lean) and the restriction bridge (BDBridge.lean).

The chart facts

theorem Hironaka.Manifold.exists_chart_of_linearIndependent_linearPart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {U : TopologicalSpace.Opens M.carrier} {y : M.carrier} (hyU : y ∈ U) (f : Fin n → ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op U))) (hf0 : ∀ (i : Fin n), ↑(f i) ⟨y, hyU⟩ = 0) {φ : OpenPartialHomeomorph M.carrier E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) (hyφ : y ∈ φ.source) (hind : LinearIndependent 𝕜 fun (i : Fin n) => (Manifold.linearPart E ψ φ hφ hyφ) ((CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ U y hyU)) (f i))) : ∃ (e : OpenPartialHomeomorph M.carrier E) (σ : Fin n ↪ Fin n), e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier ∧ y ∈ e.source ∧ e.source ⊆ ↑U ∧ ∀ x ∈ e.source, ∀ (i : Fin n), Manifold.extendSection 𝕜 E (f i) x = ψ (↑e x) (σ i)

n sections near y, vanishing at y, whose linear parts in one chart of the maximal atlas are linearly independent, are the coordinates (up to a permutation σ of the indices) of a chart of the maximal atlas at y whose source lies in their domain (exists_chart_extending for n sections, read through their linear parts).

theorem Hironaka.Manifold.exists_eq_sum_of_germ_mem_span {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {U V : TopologicalSpace.Opens M.carrier} {y : M.carrier} (hyU : y ∈ U) (hyV : y ∈ V) (s : ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op U))) {c : ℕ} (t : Fin c → ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op V))) (h : (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ U y hyU)) s ∈ Ideal.span (Set.range fun (i : Fin c) => (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.germ V y hyV)) (t i))) : ∃ (W : TopologicalSpace.Opens M.carrier) (_ : y ∈ W) (a : Fin c → ↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.obj (Opposite.op W))), ∀ x ∈ W, Manifold.extendSection 𝕜 E s x = ∑ i : Fin c, Manifold.extendSection 𝕜 E (a i) x * Manifold.extendSection 𝕜 E (t i) x

From germs to sections: a germ in the ideal spanned by finitely many germs is, on a neighbourhood, a combination of their representatives with section coefficients.

theorem Manifold.IsClosedSubmanifold.restrictStalk_coord_eq_coord_chartOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : ↑Y) {φ : OpenPartialHomeomorph M.carrier E} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) (ha : ↑a ∈ φ.source) (k : { k : Fin n // k ∉ Set.range ⇑σ }) : (hY.restrictStalk a) (coord E ψ φ ⋯ ha ↑k) = coord (Fin (n - c) → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin (n - c) → 𝕜)) (h.chartOn ⋯) ⋯ ha ((complEquiv σ) k)

The coordinates off the block: the restriction to Y of a coordinate germ of an adapted chart whose index is off the block σ is the corresponding coordinate germ of the induced chart chartOn of Y.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.frequently_notMem_of_notMem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} {c : ℕ} {φ : OpenPartialHomeomorph M.carrier E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ H φ σ) {F : HypersurfaceFamily M.carrier} {a : M.carrier} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a cidx) (ha : a ∈ H) (j : { j : F.ι // a ∈ F.hyp j }) (hj : cidx j ∉ Set.range ⇑σ) : ∃ᶠ (x : M.carrier) in nhdsWithin a H, x ∉ F.hyp ↑j

Two distinct coordinate hyperplanes: in a chart adapted to H which is a chart with simple normal crossings for F at a ∈ H, a member through a whose coordinate is off the block of H does not contain H near a (the hypothesis of IsSncChartAt.restrict_isSncChartAt).

The predicate descends to a hypersurface of maximal contact and lifts back

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.restrict_maximalContact_of_stalkIdeal_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} (hH : IsClosedSubmanifold ψ H 1) {F : HypersurfaceFamily M.carrier} {J : M.IdealSheaf} {y : M.carrier} (hle : hH.idealSheaf.stalkIdeal y ≤ IdealSheaf.stalkIdeal J y) (hy : y ∈ H) (hJy : IdealSheaf.stalkIdeal J y ≠ ⊤) (h : IsSmoothTransversalIdealAt ψ F J y) : IsSmoothTransversalIdealAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (hH.traceFamily F) (IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) ⟨y, hy⟩

The descent of the predicate ([Wlo05, Theorem 4.7.1, proof]; [Wlo09, Theorem 7.4.1]): for H a smooth hypersurface of maximal contact at the mark 1 (𝓘_H ≤ J at y), a point y ∈ H of the cosupport of J, and the predicate for (F, J) at y, the predicate holds on the bundled H for the trace family and the restriction of J at y. The equation u of H lies in J_y = (z_σ) and is not in 𝔪_y², so some coefficient is a unit and u replaces the coordinate z_{σ i₀} (exists_chart_of_linearIndependent_linearPart with the linear parts of CommonCharts.lean); in the new chart J is spanned by u and the other z_{σ i} near y (exists_eq_sum_of_germ_mem_span), the members through y stay coordinate hyperplanes, and H = {u = 0}; the induced chart of H is a chart with simple normal crossings for the trace family (IsSncChartAt.restrict_isSncChartAt, frequently_notMem_of_notMem_range) on which J|_H is spanned by the restricted coordinates (restrictStalk_coord_eq_coord_chartOn, stalkIdeal_pullback, germMap_inclusionMap, restrictStalk_coord_sub).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.restrict_maximalContact {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} (hH : IsClosedSubmanifold ψ H 1) {F : HypersurfaceFamily M.carrier} {J : M.IdealSheaf} (hle : hH.idealSheaf ≤ J) {y : M.carrier} (hy : y ∈ H) (hJy : IdealSheaf.stalkIdeal J y ≠ ⊤) (h : IsSmoothTransversalIdealAt ψ F J y) : IsSmoothTransversalIdealAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (hH.traceFamily F) (IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) ⟨y, hy⟩

The descent of the predicate ([Wlo05, Theorem 4.7.1, proof]; [Wlo09, Theorem 7.4.1]): for H a smooth hypersurface of maximal contact at the mark 1 (𝓘_H ≤ J), a point y ∈ H of the cosupport of J, and the predicate for (F, J) at y, the predicate holds on the bundled H for the trace family and the restriction of J at y: the instance of restrict_maximalContact_of_stalkIdeal_le at the inequality of stalks at y (the proof uses the hypothesis 𝓘_H ≤ J only at the point).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_restrict_maximalContact_of_eventually_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} (hH : IsClosedSubmanifold ψ H 1) {F : HypersurfaceFamily M.carrier} (hFH : HasSncWithProper ψ F H 1) {J : M.IdealSheaf} {y : M.carrier} (hle : ∀ᶠ (x : ↑↧M.carrier) in nhds y, hH.idealSheaf.stalkIdeal x ≤ IdealSheaf.stalkIdeal J x) (hy : y ∈ H) (hJy : IdealSheaf.stalkIdeal J y ≠ ⊤) (h : IsSmoothTransversalIdealAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (hH.traceFamily F) (IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) ⟨y, hy⟩) : IsSmoothTransversalIdealAt ψ F J y

The lift of the predicate ([Wlo05, Theorem 4.7.1, proof]: "since u ∈ σ^c(I) it follows that σ^c(I) = I_{Ỹ₁}"; [Wlo09, Theorem 7.4.1]): for H of maximal contact at the mark 1 (𝓘_H ≤ J near y) with F ∪ H of simple normal crossings and the members not containing H (HasSncWithProper), a point y ∈ H of the cosupport of J, and the predicate on the bundled H for the trace family and J|_H at y, the predicate holds for (F, J) at y. The cylinder argument: in the adapted chart φₐ of H with simple normal crossings for F, the retraction r onto H (the inverse of the induced chart after the projection off the block of H) makes every member a cylinder over its trace; the new ambient coordinates are the equation u of H and the cylinder extensions w_m = φ_H(r x)_m − φ_H(y)_m of all the coordinates of the chart φ_H of the hypersurface, independent because the linear parts of the w_m are those of the chart of the hypersurface (the chain rule through the projection; linearIndependent_cotangentClass_iff_linearPart) and u is transverse (exists_chart_of_linearIndependent_linearPart); in the new chart the members through y are the coordinate hyperplanes of their trace coordinates, H = {u = 0}, J = (u) + (J|_H lifted) at the points of H (ker_restrictStalk_eq_span, Ideal.comap_map_of_surjective; hJy keeps the restricted stalk proper) and J = ⊤ off H.

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_restrict_maximalContact {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} (hH : IsClosedSubmanifold ψ H 1) {F : HypersurfaceFamily M.carrier} (hFH : HasSncWithProper ψ F H 1) {J : M.IdealSheaf} (hle : hH.idealSheaf ≤ J) {y : M.carrier} (hy : y ∈ H) (hJy : IdealSheaf.stalkIdeal J y ≠ ⊤) (h : IsSmoothTransversalIdealAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (hH.traceFamily F) (IdealSheaf.pullback ⇑hH.inclusionMap ⋯ J) ⟨y, hy⟩) : IsSmoothTransversalIdealAt ψ F J y

The lift of the predicate ([Wlo05, Theorem 4.7.1, proof]; [Wlo09, Theorem 7.4.1]): for H of maximal contact at the mark 1 (𝓘_H ≤ J) with F ∪ H of simple normal crossings and the members not containing H (HasSncWithProper), a point y ∈ H of the cosupport of J, and the predicate on the bundled H for the trace family and J|_H at y, the predicate holds for (F, J) at y: the instance of of_restrict_maximalContact_of_eventually_le at the global inequality (the proof uses 𝓘_H ≤ J only on the source of its chart).