The empty-boundary bridge and the local Hadamard lemma

Two tools for the clauses of the embedded desingularization about its final strict transform (Hironaka/Resolution/Analytic/Wlo09/StrictTransformClauses.lean, Hironaka/Resolution/Analytic/Wlo09/TotalTransformClause.lean):

• The empty-boundary bridge. The shape of the final controlled transform of the modified marked resolution (output_isSmoothSubmanifoldIdeal, the output of the proof of [Wlo09, Theorem 7.4.1]) is stated on the family totalTransformSeqFrom (T|U).F grown from the restricted boundary, while the clauses of [Wlo09, Theorem 2.0.2] read the exceptional divisors as totalTransformSeq, grown from the empty family. On DomBEDan the boundary has no member, and the two families agree up to the order-preserving relabelling of their index types (F.ι ⊕ₗ PUnit ⊕ₗ … against PEmpty ⊕ₗ PUnit ⊕ₗ …); the simple-normal-crossing chart data and the predicate IsSmoothTransversalIdealAt transport along such a relabelling. (totalTransformSeqFrom_empty is the literal case F = empty, rfl.)
• The local Hadamard lemma. At a point of a chart of the maximal atlas, the vanishing ideal of the zero set of c of the chart's coordinates (a set closed in the chart's source, not in M) is the ideal spanned by those coordinates: the description of the vanishing ideal of a closed submanifold (ker_restrictStalk_eq_vanishingStalk) read on the open submanifold M.restrict φ.source, where the zero set is a closed submanifold (IsClosedSubmanifoldOn.restrict), transported back along the inclusion. Hence the stalk of an ideal sheaf that is a coordinate ideal on a chart's source is the vanishing ideal of its cosupport there (vanishingStalk_cosupport_eq_stalkIdeal_of_eq_span_coord).

Neither tool is in the sources; both are bookkeeping for the comparison of the final controlled transform with the strict transform of Y.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.of_equiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {F₁ F₂ : HypersurfaceFamily M.carrier} (e : F₁.ι ≃ F₂.ι) (he : ∀ (j : F₁.ι), F₂.hyp (e j) = F₁.hyp j) {φ : OpenPartialHomeomorph M.carrier E} {a : M.carrier} {c : { j : F₁.ι // a ∈ F₁.hyp j } → Fin n} (h : IsSncChartAt ψ F₁ φ a c) : IsSncChartAt ψ F₂ φ a fun (j : { j : F₂.ι // a ∈ F₂.hyp j }) => c ⟨e.symm ↑j, ⋯⟩

A relabelling of the index type of a family preserving the members: the data of IsSncChartAt transports.

theorem Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt.of_equiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {F₁ F₂ : HypersurfaceFamily M.carrier} (e : F₁.ι ≃ F₂.ι) (he : ∀ (j : F₁.ι), F₂.hyp (e j) = F₁.hyp j) {J : IdealSheaf (structureSheaf 𝕜 E M.carrier)} {x : M.carrier} (h : IsSmoothTransversalIdealAt ψ F₁ J x) : IsSmoothTransversalIdealAt ψ F₂ J x

A relabelling of the index type of a family preserving the members: the predicate IsSmoothTransversalIdealAt transports.

theorem Hironaka.Manifold.exists_equiv_totalTransformSeqFromAux_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) [IsEmpty F.ι] (i : ℕ) (h : i < S.length + 1) : ∃ (e : (S.totalTransformSeqFromAux F i h).ι ≃ (S.totalTransformSeqFromAux (Manifold.HypersurfaceFamily.empty M.carrier) i h).ι), ∀ (j : (S.totalTransformSeqFromAux F i h).ι), (S.totalTransformSeqFromAux (Manifold.HypersurfaceFamily.empty M.carrier) i h).hyp (e j) = (S.totalTransformSeqFromAux F i h).hyp j

The stage-indexed form of exists_equiv_totalTransformSeqFrom_of_isEmpty, by induction on the stage: at stage 0 both index types are empty; at a successor the relabelling is the sum of the previous one with the identity on the new exceptional member.

theorem Hironaka.Manifold.exists_equiv_totalTransformSeqFrom_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) [IsEmpty F.ι] (i : Fin (S.length + 1)) : ∃ (e : (S.totalTransformSeqFrom F i).ι ≃ (S.totalTransformSeq i).ι), ∀ (j : (S.totalTransformSeqFrom F i).ι), (S.totalTransformSeq i).hyp (e j) = (S.totalTransformSeqFrom F i).hyp j

The exceptional family grown from a family without members is the exceptional family grown from the empty family, up to a relabelling of the index type preserving the members.

theorem Hironaka.Manifold.isSmoothTransversalIdealAt_totalTransformSeqFrom_iff_of_isEmpty {𝕜 : 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) [IsEmpty F.ι] (i : Fin (S.length + 1)) (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E (S.stage i).carrier)) (x : (S.stage i).carrier) : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ (S.totalTransformSeqFrom F i) J x ↔ Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ (S.totalTransformSeq i) J x

The empty-boundary bridge for the predicate IsSmoothTransversalIdealAt: on a boundary without members, the predicate on totalTransformSeqFrom F i is the predicate on totalTransformSeq i.

theorem Hironaka.Manifold.vanishingStalk_zeroSet_eq_span_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {φ : OpenPartialHomeomorph M.carrier E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {x : M.carrier} (hx : x ∈ φ.source) {c : ℕ} (σ : Fin c ↪ Fin n) (h0 : ∀ (i : Fin c), ψ (↑φ x) (σ i) = 0) : Manifold.vanishingStalk (φ.source ∩ {y : M.carrier | ∀ (i : Fin c), ψ (↑φ y) (σ i) = 0}) x = Ideal.span (Set.range fun (i : Fin c) => Manifold.coord E ψ φ hφ hx (σ i))

The local Hadamard lemma (the vanishing ideal of a closed submanifold, on the open submanifold of a chart's source): at a point x of a chart φ of the maximal atlas where the coordinates z_σ vanish, the vanishing ideal of the zero set {z_σ = 0} ∩ φ.source is spanned by those coordinates.

theorem Hironaka.Manifold.vanishingStalk_cosupport_eq_stalkIdeal_of_eq_span_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M.carrier)) {φ : OpenPartialHomeomorph M.carrier E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M.carrier) {c : ℕ} (σ : Fin c ↪ Fin n) (hJ : ∀ (a : M.carrier) (ha : a ∈ φ.source), J.stalkIdeal a = Ideal.span (Set.range fun (i : Fin c) => Manifold.coord E ψ φ hφ ha (σ i))) {x : M.carrier} (hx : x ∈ φ.source) : Manifold.vanishingStalk J.support x = J.stalkIdeal x

The stalk of an ideal sheaf which is a coordinate ideal on a chart's source equals the vanishing ideal of its cosupport at every point of the source: the local Hadamard lemma for a smooth submanifold ideal (the shape the final controlled transform has at a support point).