The two stop clauses across a change of boundary family

The output clause and the stopped clause of ClauseTools.lean (the fields output_isSmoothSubmanifoldIdeal and stopped_never_blownUp of BMOmodFam) are stated against the total boundary of the run; the pieces of the modified first step satisfy them against other boundary families. The boundary of the triple of [Kol07, Theorem 103, Step 2.2] (the exceptional divisors of Step 2.1 with the maximal-contact member H_r emptied) is a sub-family of the total boundary at that stage, the members present before Step 2.1 being dropped; and the boundary of the run one dimension down is identified with the trace of the ambient boundary on the strict transforms of H⁺ at the level of supports only (support_traceFamilyFrom_eq_support_boundarySeq, boundarySeq_pushforwardStageIso, isSnc_totalTransformSeqFrom_and_boundarySeq_eq). This module proves the generic bridges, for arbitrary boundary families:

• HypersurfaceFamily.MembersSubset F' F: every nonempty member of F' is a member of F. The relation is kept by inverse images, by the total transform under a blow-up (equal members have equal strict transforms, the exceptional member is shared) and hence along the boundary families of a succession (membersSubset_totalTransformSeqFrom); the exceptional divisors alone form a sub-family of every boundary family (membersSubset_totalTransformSeq_totalTransformSeqFrom).
• IsSmoothTransversalIdealAt.of_membersSubset: the predicate passes to a sub-family (IsSmoothTransversalIdealAt.emptyMember is the one-member case); IsSmoothTransversalIdealAt.of_forall_mem: and back when every member of the bigger family through the point is a member of the smaller one (the situation of the output clause, where the extra members miss the support of the transform).
• IsSnc.exists_hyp_inter_eq_of_support_eq, IsSnc.exists_equiv_of_support_eq_nhds, IsSmoothTransversalIdealAt.of_support_eq_nhds: two families with simple normal crossings and the same support near a point have the same members through it near it, so the predicate depends only on the support of the boundary near the point. On the open the member is a closed hypersurface having simple normal crossings with one family, hence, by the dictionary hasOnlyNormalCrossingsWith_idealSheaf_iff on the reduced ideal sheaves, which agree on the open, with the other; in a chart with simple normal crossings it is a coordinate hyperplane inside the finite union of the coordinate hyperplanes of the members through the point, hence one of them (exists_mem_source_coord_eq_zero_ne: a coordinate hyperplane is not contained in a finite union of other coordinate hyperplanes near a point; IsSncChartAt.eq_of_hyp_inter_eq, IsSnc.hyp_injOn_nonempty); then IsSmoothTransversalIdealAt.congr_nhds.
• StoppedClause.of_membersSubset, OutputClause.of_forall_mem: the same bridges for the two clauses.
• notMem_center_of_ord_eq_zero: a point of order 0 is never blown up. A centre point has order ≥ 1 ([Kol07, Definition 66 (4′)]), and the marked transform at a point over a point off the centre is the pull-back of the stalk below (birationalTransform_stalkIdeal_of_notMem); an induction on the first stage at which the fibre would meet a centre, from the order clause alone; the stop predicate does not enter.

The relation between the boundary of the run on a hypersurface and the trace of the ambient boundary is the E_i ∩ S_i of [Kol07, Definition 30, 30.2]; the order of a centre is [Kol07, Definition 66 (4′)]; simple normal crossings are [Kol07, Definition 24] and [Wlo09, Theorem 2.0.3 (2)]. The statements themselves are not in the sources.

def Manifold.HypersurfaceFamily.MembersSubset {M : Type u} (F' F : HypersurfaceFamily M) : Prop

The sub-family relation: every nonempty member of F' is a member of F (as a set). This is the relation between the boundary of the triple of [Kol07, Theorem 103, Step 2.2] (the exceptional divisors of Step 2.1, H_r emptied) and the total boundary at that stage: the members present before Step 2.1 are dropped, and H_r is a member of neither.

Equations

• F'.MembersSubset F = ∀ (j' : F'.ι), F'.hyp j' = ∅ ∨ ∃ (j : F.ι), F'.hyp j' = F.hyp j

theorem Manifold.HypersurfaceFamily.MembersSubset.support_subset {M : Type u} {F' F : HypersurfaceFamily M} (h : F'.MembersSubset F) : F'.support ⊆ F.support

The support of a sub-family lies in the support.

theorem Manifold.HypersurfaceFamily.membersSubset_empty {M : Type u} (F : HypersurfaceFamily M) : (empty M).MembersSubset F

The empty family is a sub-family of every family.

theorem Manifold.HypersurfaceFamily.membersSubset_emptyMember {M : Type u} (F : HypersurfaceFamily M) (j : F.ι) : (F.emptyMember j).MembersSubset F

A family with one member emptied is a sub-family of the family.

theorem Manifold.HypersurfaceFamily.MembersSubset.comap {M N : Type u} {F' F : HypersurfaceFamily M} (h : F'.MembersSubset F) (g : N → M) : (HypersurfaceFamily.comap g F').MembersSubset (HypersurfaceFamily.comap g F)

The sub-family relation is kept by inverse images.

theorem Manifold.HypersurfaceFamily.MembersSubset.totalTransform {M M' : Type u} [TopologicalSpace M'] {F' F : HypersurfaceFamily M} (h : F'.MembersSubset F) (π : M' → M) (Y : Set M) : (HypersurfaceFamily.totalTransform π Y F').MembersSubset (HypersurfaceFamily.totalTransform π Y F)

The sub-family relation is kept by the total transform under a blow-up: equal members have equal strict transforms, the empty member an empty one, and the exceptional member is shared.

theorem AnalyticManifold.FiniteSuccession.membersSubset_totalTransformSeqFrom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F' F : Manifold.HypersurfaceFamily M.carrier} (h : F'.MembersSubset F) (i : Fin (S.length + 1)) : (S.totalTransformSeqFrom F' i).MembersSubset (S.totalTransformSeqFrom F i)

The sub-family relation is kept by the boundary families of a succession at every stage (MembersSubset.totalTransform along the recursion of totalTransformSeqFromAux).

theorem AnalyticManifold.FiniteSuccession.membersSubset_totalTransformSeq_totalTransformSeqFrom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : Fin (S.length + 1)) : (S.totalTransformSeq i).MembersSubset (S.totalTransformSeqFrom F i)

The exceptional divisors alone (the boundary family from the empty start) form a sub-family of the boundary family from any start F.

theorem Hironaka.Manifold.exists_mem_source_coord_eq_zero_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (K : Finset (Fin n)) {k : Fin n} (hk : k ∉ K) (h0 : ψ (↑φ a) k = 0) (hK : ∀ c ∈ K, ψ (↑φ a) c = 0) {W : Set M} (hW : W ∈ nhds a) : ∃ y ∈ φ.source ∩ W, ψ (↑φ y) k = 0 ∧ ∀ c ∈ K, ψ (↑φ y) c ≠ 0

A coordinate hyperplane of a chart is not contained in a finite union of other coordinate hyperplanes near a point: in a chart φ at a, for finitely many indices K and an index k ∉ K whose coordinates all vanish at a, every neighbourhood of a contains a point of the source where the k-th coordinate vanishes and none of the K-coordinates does (the point ψ⁻¹(ψ (φ a) + ε · 1_K) for a small ε ≠ 0).

theorem Manifold.HypersurfaceFamily.IsSncChartAt.eq_of_hyp_inter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} {φ : OpenPartialHomeomorph M.carrier E} {x : M.carrier} {c : { j : F.ι // x ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ x c) {W : Set M.carrier} (hW : W ∈ nhds x) {j₁ j₂ : { j : F.ι // x ∈ F.hyp j }} (h : F.hyp ↑j₁ ∩ W = F.hyp ↑j₂ ∩ W) : j₁ = j₂

Two members through x of a family with simple normal crossings that agree near x are the same member: in the chart at x they are coordinate hyperplanes with the same trace near x, so their indices agree (exists_mem_source_coord_eq_zero_ne), and cidx is injective.

theorem Manifold.HypersurfaceFamily.IsSnc.hyp_injOn_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ F) {j₁ j₂ : F.ι} (h : F.hyp j₁ = F.hyp j₂) (hne : (F.hyp j₁).Nonempty) : j₁ = j₂

A family with simple normal crossings has no two indices with the same nonempty member (IsSncChartAt.eq_of_hyp_inter_eq at a point of the member, with W = univ).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_membersSubset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F' F : HypersurfaceFamily M.carrier} (hF' : IsSnc ψ F') (hsub : F'.MembersSubset F) {J : M.IdealSheaf} {x : M.carrier} (h : IsSmoothTransversalIdealAt ψ F J x) : IsSmoothTransversalIdealAt ψ F' J x

The predicate passes to a sub-family (the bigger boundary implies the smaller; IsSmoothTransversalIdealAt.emptyMember is the one-member case): the members of F' through x inject into those of F through x with the same sets, and the chart, the coordinates σ and the ideal are unchanged.

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_forall_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F' F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ F) {x : M.carrier} (hall : ∀ (j : F.ι), x ∈ F.hyp j → ∃ (j' : F'.ι), F'.hyp j' = F.hyp j) {J : M.IdealSheaf} (h : IsSmoothTransversalIdealAt ψ F' J x) : IsSmoothTransversalIdealAt ψ F J x

The predicate passes back from a sub-family when every member of the bigger family through the point is one of the sub-family (IsSmoothTransversalIdealAt.congr_nhds with an equivalence of the members through x). This is the situation of the output clause, where the extra members miss the support of the transform.

theorem Manifold.HypersurfaceFamily.IsSnc.exists_hyp_inter_eq_of_support_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F₁ F₂ : HypersurfaceFamily M.carrier} (hF₁ : IsSnc ψ F₁) (hF₂ : IsSnc ψ F₂) {U : Set M.carrier} (hU : IsOpen U) {x : M.carrier} (hxU : x ∈ U) (hsupp : F₁.support ∩ U = F₂.support ∩ U) (j₂ : { j : F₂.ι // x ∈ F₂.hyp j }) : ∃ (j₁ : { j : F₁.ι // x ∈ F₁.hyp j }) (V : Set M.carrier), IsOpen V ∧ x ∈ V ∧ F₁.hyp ↑j₁ ∩ V = F₂.hyp ↑j₂ ∩ V

A member of F₂ through x is, near x, a member of F₁, for families with simple normal crossings and the same support on an open U ∋ x (the E_i ∩ S_i of [Kol07, Definition 30, 30.2] read member by member). On U the member is a closed hypersurface having simple normal crossings with F₂|U, hence, by the dictionary hasOnlyNormalCrossingsWith_idealSheaf_iff on the reduced ideal sheaves, which agree on U (idealSheaf_congr_support), with F₁|U; in the chart of F₁ at x it is a coordinate hyperplane inside the finite union of the coordinate hyperplanes of the members of F₁ through x (the other members miss a neighbourhood, LocallyFinite.iInter_compl_mem_nhds), so by exists_mem_source_coord_eq_zero_ne it is one of them.

theorem Manifold.HypersurfaceFamily.IsSnc.exists_equiv_of_support_eq_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F₁ F₂ : HypersurfaceFamily M.carrier} (hF₁ : IsSnc ψ F₁) (hF₂ : IsSnc ψ F₂) {U : Set M.carrier} (hU : IsOpen U) {x : M.carrier} (hxU : x ∈ U) (hsupp : F₁.support ∩ U = F₂.support ∩ U) : ∃ (e : { j : F₁.ι // x ∈ F₁.hyp j } ≃ { j : F₂.ι // x ∈ F₂.hyp j }) (V : Set M.carrier), IsOpen V ∧ x ∈ V ∧ ∀ (j : { j : F₁.ι // x ∈ F₁.hyp j }), F₂.hyp ↑(e j) ∩ V = F₁.hyp ↑j ∩ V

Two families with simple normal crossings and the same support near x have the same members through x near x: IsSnc.exists_hyp_inter_eq_of_support_eq in both directions, the two maps inverse to each other by IsSncChartAt.eq_of_hyp_inter_eq, on the finite intersection of the neighbourhoods (finitely many members through x, LocallyFinite.point_finite).

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_support_eq_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F₁ F₂ : HypersurfaceFamily M.carrier} (hF₁ : IsSnc ψ F₁) (hF₂ : IsSnc ψ F₂) {U : Set M.carrier} (hU : IsOpen U) {x : M.carrier} (hxU : x ∈ U) (hsupp : F₁.support ∩ U = F₂.support ∩ U) {J : M.IdealSheaf} (h : IsSmoothTransversalIdealAt ψ F₁ J x) : IsSmoothTransversalIdealAt ψ F₂ J x

The predicate depends only on the support of the boundary near the point, for families with simple normal crossings: IsSnc.exists_equiv_of_support_eq_nhds and IsSmoothTransversalIdealAt.congr_nhds. This is the bridge between the boundary of the run one dimension down and the trace of the ambient boundary along a push-forward, which the library identifies at the level of supports and reduced ideal sheaves only (support_traceFamilyFrom_eq_support_boundarySeq, boundarySeq_pushforwardStageIso, isSnc_totalTransformSeqFrom_and_boundarySeq_eq).

theorem AnalyticManifold.FiniteSuccession.StoppedClause.of_membersSubset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I : M.IdealSheaf} {F' F : Manifold.HypersurfaceFamily M.carrier} (hsnc : ∀ (i : Fin (S.length + 1)), Manifold.HypersurfaceFamily.IsSnc ψ₀ (S.totalTransformSeqFrom F' i)) (hsub : F'.MembersSubset F) (h : StoppedClause ψ₀ S I F') : StoppedClause ψ₀ S I F

The stopped clause passes from a sub-family boundary to the bigger boundary: a predicate point off the bigger boundary is a predicate point off the smaller one (IsSmoothTransversalIdealAt.of_membersSubset at its stage, membersSubset_totalTransformSeqFrom, MembersSubset.support_subset).

theorem AnalyticManifold.FiniteSuccession.OutputClause.of_forall_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I : M.IdealSheaf} {F' F : Manifold.HypersurfaceFamily M.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ (S.totalTransformSeqFrom F (Fin.last S.length))) (hall : ∀ (x : (S.stage (Fin.last S.length)).carrier), 1 ≤ Manifold.IdealSheaf.ord (S.markedTransformSeq I 1 (Fin.last S.length)) x → ∀ (j : (S.totalTransformSeqFrom F (Fin.last S.length)).ι), x ∈ (S.totalTransformSeqFrom F (Fin.last S.length)).hyp j → ∃ (j' : (S.totalTransformSeqFrom F' (Fin.last S.length)).ι), (S.totalTransformSeqFrom F' (Fin.last S.length)).hyp j' = (S.totalTransformSeqFrom F (Fin.last S.length)).hyp j) (h : OutputClause ψ₀ S I F') : OutputClause ψ₀ S I F

The output clause passes from a sub-family boundary to the bigger boundary when every member of the bigger boundary through a support point of the last stage is a member of the smaller one (IsSmoothTransversalIdealAt.of_forall_mem at the last stage).

theorem AnalyticManifold.FiniteSuccession.notMem_center_of_ord_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} (hge : S.IsOfOrderGe I 1 E₀) (i k : ℕ) (h : i + k < S.length) {x : (S.stage ⟨i, ⋯⟩).carrier} (hx : Manifold.IdealSheaf.ord (S.markedTransformSeq I 1 ⟨i, ⋯⟩) x = 0) (y : (S.stage ⟨i + k, ⋯⟩).carrier) (hy : (S.stageMapAdd i k ⋯) y = x) : y ∉ Manifold.IdealSheaf.support (S.center ⟨i + k, h⟩)

A point of order 0 is never blown up, along a succession of order ≥ 1: a centre point has order ≥ 1 along the centre, hence order ≥ 1 ([Kol07, Definition 66 (4′)]), so a point of order 0 is not in the centre, and the marked transform at a point over it is the pull-back of the stalk below (birationalTransform_stalkIdeal_of_notMem, the blow-up being a local isomorphism there), of order 0 again. The proof is an induction on the number of steps; no predicate is involved.