The stop predicate: persistence off the centres, and the stopped germ

The structure BMOmodFam carries two clauses about the predicate IsSmoothTransversalIdealAt ψ F J x, "J is at x locally the ideal of a smooth submanifold with coordinates transversal to F" (the output of the modified algorithm, locally equal to I″ = (u₁, …, u_k) "where u_i are coordinates transversal to exceptional divisors", [Wlo09, Theorem 7.4.1]): the output of the modified functor satisfies it at every point of the support, and a point at which it holds and which lies on no boundary member is never blown up again. Both proofs walk the succession past the point: one needs to know that the predicate, once true at a point off the centres, stays true at the points over it, and that no exceptional divisor ever passes through them. This module proves those persistence facts and the two germ facts of the stopped case, at a general model ψ:

• Locality and transport. IsSmoothTransversalIdealAt.congr_nhds: the predicate at x depends only on the members through x near x and on the stalks near x; the chart with simple normal crossings is restricted to the open set where the data agree (IsSncChartAt.restrOpen), its coordinate germs unchanged (coord_eq_coord_of_eventuallyEq). IsSmoothTransversalIdealAt.comap: the predicate transports along a local analytic isomorphism g at y; the chart at g y is composed with the local inverse (transportChart), the coordinate germs pulled back (germMap_coord_eq_coord_transportChart), the stalks of comap g J the images of the stalks of J (stalkIdeal_comap_eq_map_germMap).
• One blow-up off the centre (a blow-up is an isomorphism off its centre, and the exceptional divisor lies over the centre). IsSmoothTransversalIdealAt.totalTransform_of_notMem: for π y ∉ Y and 𝓘 of order ≥ 1 along Y, the predicate for (E, 𝓘) at π y gives it for the total transform of E and the marked transform of (𝓘, 1) at y; transport along IsBlowUp.isLocalDiffeomorphOn_compl, then locality on π⁻¹(Yᶜ), where the marked transform is the pull-back (birationalTransform_stalkIdeal_of_notMem) and the strict transforms of the members through π y are their preimages (mem_strictTransformSet_iff_of_notMem), the exceptional member missing y. notMem_totalTransform_of_notMem: a point off the exceptional divisor whose image is on no member is on no member of the total transform.
• Along a succession. FiniteSuccession.notMem_totalTransformSeqFrom_of_forall_notMem_center: a point y at stage i + k over x at stage i (stageMapAdd), with x on no member of E_i and no intermediate centre containing a point over x, is on no member of E_{i+k}; induction on k with the previous fact at each stage, the boundaries having simple normal crossings by isSnc_totalTransformSeqFrom_and_boundarySeq_eq from the normal-crossings clause of IsOfOrderGe. The hypothesis quantifies over all points over x at the intermediate stages, the form the induction for the second clause produces.
• The stopped germ ("if I′ = (u) is the ideal of smooth hypersurface … the algorithm is stopped", [Wlo09, Theorem 7.4.1]). ord_le_one_of_isSmoothTransversalIdealAt: at a point where the predicate holds with nonzero stalk, ord J ≤ 1, a coordinate germ lying in J_x ∖ 𝔪_x² (coord_notMem_maximalIdeal_sq). isSmoothTransversalIdealAt_of_eq_idealSheaf: if 𝓘 is the ideal sheaf of the smooth hypersurface H near y ∈ H and no member passes through y, the predicate holds with c = 1; an adapted chart of H restricted to where the sheaves agree, 𝓘_a = (z_{σ 0}) on H (stalkIdeal_idealSheaf_eq_span), = ⊤ off H (the coordinate a unit there).
• The stopped locus. BD.mem_Zminus1_one_iff_isHypersurfaceIdealAt: for H of maximal contact at the mark 1 (𝓘_H ≤ 𝓘, [Wlo09, Lemma 5.5.1 (1)]) and x ∈ H, x ∈ Z_{-1}(𝓘, 1, H) (the component of x in H lies in {ord 𝓘 ≥ 1}, BD.Zminus1) iff 𝓘 = 𝓘_H stalkwise near x, the germ characterisation which the previous fact uses. Both directions read the stalks of 𝓘|_H through IsClosedSubmanifold.stalkIdeal_pullback_inclusionMap_eq_bot_iff (the restriction of germs: (𝓘|_H)_a = 0 ⇔ 𝓘_a ≤ (𝓘_H)_a) and IdealSheaf.stalkIdeal_eq_bot_of_eventually_mem_support (a cosupport containing a neighbourhood of a forces a zero stalk). Backwards, {(𝓘|_H)_a = 0} is clopen in H (isClopen_setOf_stalkIdeal_eq_bot, the identity theorem) and contains the component; forwards, on an adapted chart of H at x meeting H inside the component (exists_adaptedChart_source_inter_subset), ord 𝓘 ≥ 1 on H puts a whole neighbourhood into the cosupport of 𝓘|_H.

The restriction of the predicate to the hypersurface of maximal contact and back (restrict_maximalContact, of_restrict_maximalContact) is StopRestrict.lean.

Locality and transport of the predicate

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.congr_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {F₁ F₂ : HypersurfaceFamily M.carrier} {J₁ J₂ : M.IdealSheaf} {x : M.carrier} {U : Set M.carrier} (hU : IsOpen U) (hxU : x ∈ U) (e : { j : F₁.ι // x ∈ F₁.hyp j } ≃ { j : F₂.ι // x ∈ F₂.hyp j }) (he : ∀ (j : { j : F₁.ι // x ∈ F₁.hyp j }), F₂.hyp ↑(e j) ∩ U = F₁.hyp ↑j ∩ U) (hJ : ∀ a ∈ U, IdealSheaf.stalkIdeal J₁ a = IdealSheaf.stalkIdeal J₂ a) (h : IsSmoothTransversalIdealAt ψ F₁ J₁ x) : IsSmoothTransversalIdealAt ψ F₂ J₂ x

The locality of the predicate: the predicate at x depends only on the members through x near x (an equivalence e of the members through x, equal on an open U ∋ x) and on the stalks of the ideal on U; the chart with simple normal crossings is restricted to U (IsSncChartAt.restrOpen), its coordinate germs are those of the chart (coord_eq_coord_of_eventuallyEq).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M N : AnalyticManifold 𝕜 E} (F : HypersurfaceFamily M.carrier) (J : M.IdealSheaf) (g : AnalyticMap N M) {y : N.carrier} (hg : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑g) y) (h : IsSmoothTransversalIdealAt ψ F J (g y)) : IsSmoothTransversalIdealAt ψ (HypersurfaceFamily.comap (⇑g) F) (IdealSheaf.pullback ⇑g ⋯ J) y

The predicate transports along a local analytic isomorphism g at y: the chart at g y composed with the local inverse (transportChart, transportChart_mem_maximalAtlas), the coordinate germs pulled back (germMap_coord_eq_coord_transportChart), the stalks of comap g J the images of the stalks of J (stalkIdeal_comap_eq_map_germMap, Ideal.map_span); the members through y of F.comap g are those of F through g y.

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.totalTransform_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {n₁ : ℕ} {ψ₁ : E ≃L[𝕜] Fin n₁ → 𝕜} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₁ Y c) {M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} (h : IsBlowUp ψ₁ Y c π) {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ F) {J : M.IdealSheaf} (hJ : ∀ a ∈ Y, 1 ≤ hY.idealSheaf.ordAlongIdeal J a) {y : M'.carrier} (hy : π y ∉ Y) (hP : IsSmoothTransversalIdealAt ψ F J (π y)) : IsSmoothTransversalIdealAt ψ (totalTransform π Y F) (MarkedIdealSheaf.birationalTransform hY h { I := J, m := 1 }).I y

One blow-up, off the centre: for a blow-up π with centre Y (any model ψ₁), an ideal sheaf 𝓘 of order ≥ 1 along Y (the hypothesis hJ, the standing condition for the marked transform of (𝓘, 1)) and a point y with π y ∉ Y, the predicate for (E, 𝓘) at π y gives the predicate for the total transform of E and the marked transform of (𝓘, 1) at y. The blow-up is a local analytic isomorphism at y (IsBlowUp.isLocalDiffeomorphOn_compl), the marked transform is the pull-back off the centre (birationalTransform_stalkIdeal_of_notMem), the strict transforms of the members through π y are their preimages near y (mem_strictTransformSet_iff_of_notMem) and the exceptional member misses y: transport, then locality.

theorem Manifold.HypersurfaceFamily.notMem_totalTransform_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {n₁ : ℕ} {ψ₁ : E ≃L[𝕜] Fin n₁ → 𝕜} {Y : Set M.carrier} {c : ℕ} {M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} (h : IsBlowUp ψ₁ Y c π) {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ F) {y : M'.carrier} (hy : π y ∉ Y) (hx : ∀ (j : F.ι), π y ∉ F.hyp j) (j : (totalTransform π Y F).ι) : y ∉ (totalTransform π Y F).hyp j

One step along a succession: a point y off the exceptional divisor whose image lies on no member of E lies on no member of the total transform of E; the strict transform of a member is its preimage off the centre (mem_strictTransformSet_iff_of_notMem), the exceptional member is π⁻¹(Y).

theorem AnalyticManifold.FiniteSuccession.notMem_totalTransformSeqFrom_of_forall_notMem_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (h3 : ∀ (i : Fin S.length), (S.boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith (S.center i)) (i k : ℕ) (h : i + k < S.length + 1) {x : (S.stage ⟨i, ⋯⟩).carrier} (hx : ∀ (j : (S.totalTransformSeqFrom F ⟨i, ⋯⟩).ι), x ∉ (S.totalTransformSeqFrom F ⟨i, ⋯⟩).hyp j) (hcen : ∀ (l : ℕ) (hl : l < k) (z : (S.stage ⟨i + l, ⋯⟩).carrier), (S.stageMapAdd i l ⋯) z = x → z ∉ Manifold.IdealSheaf.support (S.center ⟨i + l, ⋯⟩)) (y : (S.stage ⟨i + k, h⟩).carrier) (hy : (S.stageMapAdd i k h) y = x) (j : (S.totalTransformSeqFrom F ⟨i + k, h⟩).ι) : y ∉ (S.totalTransformSeqFrom F ⟨i + k, h⟩).hyp j

Along a succession, a point y at stage i + k over x (stageMapAdd), with x on no member of the boundary E_i and no intermediate centre containing a point over x, lies on no member of E_{i+k}: induction on k with notMem_totalTransform_of_notMem at each stage (totalTransformSeqFrom_succ, stageMapAdd_succ; the boundaries have simple normal crossings by isSnc_totalTransformSeqFrom_and_boundarySeq_eq from the normal-crossings clause h3).

theorem Hironaka.Manifold.ord_le_one_of_isSmoothTransversalIdealAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {F : Manifold.HypersurfaceFamily M.carrier} {J : M.IdealSheaf} {x : M.carrier} (hJ : Manifold.IdealSheaf.stalkIdeal J x ≠ ⊥) (h : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ F J x) : Manifold.IdealSheaf.ord J x ≤ 1

At a point where the predicate holds the ideal is spanned by coordinates of a chart (c = 0 excluded by a nonzero stalk), so its order is at most 1: the coordinate z_{σ 0} lies in J_x ∖ 𝔪_x² (coord_notMem_maximalIdeal_sq).

The stopped case and the germ characterisation of the stopped locus

theorem Manifold.HypersurfaceFamily.isSmoothTransversalIdealAt_of_eq_idealSheaf {𝕜 : 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} (hy : y ∈ H) (hJ : ∀ᶠ (a : ↑↧M.carrier) in nhds y, IdealSheaf.stalkIdeal J a = hH.idealSheaf.stalkIdeal a) (hF : ∀ (j : F.ι), y ∉ F.hyp j) : IsSmoothTransversalIdealAt ψ F J y

The stopped case ("if I′ = (u) is the ideal of smooth hypersurface … the algorithm is stopped", [Wlo09, Theorem 7.4.1]): if 𝓘 is the ideal sheaf of the smooth hypersurface H near y ∈ H and no member of E passes through y, the predicate holds at y with c = 1. An adapted chart of H at y (exists_adaptedChart) is restricted to where the two ideal sheaves agree (IsAdaptedChart.restrOpen'); 𝓘_a = (z_{σ 0}) at the points of H (IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_span) and = ⊤ = (z_{σ 0}) off H (the coordinate a unit there, isUnit_coord_of_ne_zero); no member passes through y, so the clause on the members of the chart has nothing to check.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_pullback_inclusionMap_eq_bot_iff {𝕜 : 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) (J : M.IdealSheaf) {a : M.carrier} (ha : a ∈ S) : (IdealSheaf.pullback ⇑hS.inclusionMap ⋯ J).stalkIdeal ⟨a, ha⟩ = ⊥ ↔ IdealSheaf.stalkIdeal J a ≤ hS.idealSheaf.stalkIdeal a

The restriction of germs to a closed submanifold: the pull-back of J to the bundled closed submanifold S has zero stalk at a ∈ S iff the stalk of J at a lies in the vanishing ideal of S there (stalkIdeal_pullback, Ideal.map_eq_bot_iff_le_ker, germMap_inclusionMap, the germ map of the inclusion being restrictStalk; stalkIdeal_idealSheaf_of_mem, the kernel form of 𝓘_S).

theorem Manifold.IdealSheaf.stalkIdeal_eq_bot_of_eventually_mem_support {𝕜 : Type} [RCLike 𝕜] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {X : Type u} [TopologicalSpace X] [ChartedSpace E' X] (J : IdealSheaf (structureSheaf 𝕜 E' X)) {a : X} (h : ∀ᶠ (b : ↑↧X) in nhds a, b ∈ J.support) : J.stalkIdeal a = ⊥

The identity of germs, in neighbourhood form: an ideal sheaf whose cosupport contains a neighbourhood of a has zero stalk at a; its local generators vanish at every point near a (mem_cosupport_iff_forall_eq_zero), so their germs are zero (germ_eq_zero_iff).

theorem Hironaka.Manifold.BD.mem_Zminus1_one_iff_isHypersurfaceIdealAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) {J : M.IdealSheaf} (hle : hH.idealSheaf ≤ J) {x : M.carrier} (hx : x ∈ H) : x ∈ Zminus1 J 1 H ↔ ∀ᶠ (a : ↑↧M.carrier) in nhds x, Manifold.IdealSheaf.stalkIdeal J a = hH.idealSheaf.stalkIdeal a

The germ characterisation of the stopped locus at the mark 1 ([Wlo09, Theorem 7.4.1], "the algorithm is stopped"; the maximal-contact element lies in the ideal at µ = 1, [Wlo09, Lemma 5.5.1 (1)]): for a smooth hypersurface H of maximal contact at the mark 1 (𝓘_H ≤ 𝓘) and x ∈ H, x ∈ Z_{-1} (the connected component of x in H lies in {ord 𝓘 ≥ 1}, BD.Zminus1) iff 𝓘 is the ideal sheaf of H near x. Both directions read the stalks of 𝓘|_H through stalkIdeal_pullback_inclusionMap_eq_bot_iff ((𝓘|_H)_a = 0 ⇔ 𝓘_a ≤ 𝓘_{H,a}, hence ⇔ 𝓘_a = 𝓘_{H,a} under 𝓘_H ≤ 𝓘). Forwards, an adapted chart of H at x whose source meets H inside the component (exists_adaptedChart_source_inter_subset): on the source, off H both stalks are the unit ideal, and at a ∈ H every point of H near a has ord 𝓘 ≥ 1, so 𝓘|_H has the whole neighbourhood in its cosupport and zero stalk at a (stalkIdeal_eq_bot_of_eventually_mem_cosupport). Backwards, (𝓘|_H)_x = 0, and {(𝓘|_H)_a = 0} is clopen in H (isClopen_setOf_stalkIdeal_eq_bot, the identity theorem), so it contains the component, along which 𝓘_a = 𝓘_{H,a} ≠ 𝒪_a gives ord 𝓘 ≥ 1.