The local-isomorphism equivalence on a neighbourhood of a point

The propagation step of Kollár's proof of the uniqueness of maximal contact [Kol07, 95]: the conditions (91.1′–4′), established at p, also hold in an open neighbourhood U(p) of p, by Krull's intersection theorem [Kol07, Definition 55]. The coordinate swap of Hironaka/Resolution/Analytic/MaximalContact/SwapRealizes.lean (exists_realizing_swap) gives, at a point p of cosupp(I, m), two charts e, e' centred at p, the swap Φ = e'⁻¹ ∘ e (a partial analytic isomorphism fixing p) and its pull-back of germs r = Φ^* with r(I_{H'}) = I_H, r(I_p) = I_p, r(I_{E^j}) = I_{E^j} and s − r s ∈ MC(I)_p. This module spreads these four stalk-level identities to a neighbourhood:

• on the open submanifold N := Φ.source, with ι₀ : N → M the inclusion and Φ₀ := Φ ∘ ι₀, the stalk map of Φ₀ at p is ι₀^* ∘ r, so Φ₀^*J and ι₀^*J have the same stalk at p for J = I, I_H/I_{H'}, I_{E^j}; two ideal sheaves with the same stalk at a point agree on a neighbourhood (IdealSheaf.exists_opens_forall_stalkIdeal_eq — Kollár's "(55)", Krull's intersection theorem [Kol07, Definition 55], through eventually_stalkIdeal_le), and their cosupports then agree there: (1′), (2′) and (3′) for the finitely many E^j meeting a neighbourhood of p (local finiteness of the snc family; the other components miss both U(p) and Φ(U(p)));
• (4′): the coordinate defects dᵢ := e'ᵢ − e'ᵢ ∘ Φ are sections near p whose germs at p are e'ᵢ − r(e'ᵢ) ∈ MC(I)_p, hence lie in MC(I) near p (eventually_germ_mem_stalkIdeal). At a point q of V(MC(I)) all dᵢ(q) = 0, so e'(Φ q) = e'(q) and Φ q = q; and the two stalk maps ι^*, Φ^* at q agree on the constants and differ on the coordinate germs e'ᵢ by the germs of the dᵢ, hence differ by MC(I)_q on every germ (the coordinate criterion sub_mem_of_forall_coord_sub_mem) — AgreeOnSubspace ι Φ (MC(ι^*I)), the derivatives commuting with the restriction to the open subset (iteratedDeriv_restrictOpens).

U(p) is the intersection of these neighbourhoods; Φ : U(p) → M is a local analytic isomorphism and an open embedding (PartialDiffeomorph.isLocalDiffeomorph_comp_subtype_val). Włodarczyk's glueing automorphism has the same properties on a neighbourhood [Wlo09, Lemma 5.5.3, proof, (1)]. The neighbourhoods are assembled into a covering in Hironaka/Resolution/Analytic/MaximalContact/Covering.lean.

theorem Hironaka.Manifold.locallyIsoEquivalent_on_nhd {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {m : ℕ} (hm : 1 ≤ m) (hI : Manifold.IdealSheaf.iteratedDeriv I (m - 1) * Manifold.IdealSheaf.deriv I ≤ I) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {H H' : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ H 1) (hH' : Manifold.IsClosedSubmanifold ψ H' 1) (hHmc : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (hH'mc : hH'.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv I (m - 1)) (hHF : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H)) (hH'F : Manifold.HypersurfaceFamily.IsSnc ψ (F.append H')) (p : M.carrier) (hp : Manifold.IdealSheaf.ord I p = ↑m) : ∃ (U : TopologicalSpace.Opens M.carrier) (hpU : p ∈ U) (Φ : AnalyticMap (M.restrict U) M), IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑Φ ∧ Topology.IsOpenEmbedding ⇑Φ ∧ Φ ⟨p, hpU⟩ = p ∧ ⇑(M.inclusion U) ⁻¹' H = ⇑Φ ⁻¹' H' ∧ Manifold.IdealSheaf.pullback ⇑(M.inclusion U) ⋯ I = Manifold.IdealSheaf.pullback ⇑Φ ⋯ I ∧ (∀ (j : F.ι), ⇑(M.inclusion U) ⁻¹' F.hyp j = ⇑Φ ⁻¹' F.hyp j) ∧ AgreeOnSubspace (M.inclusion U) Φ ((Manifold.IdealSheaf.pullback ⇑(M.inclusion U) ⋯ I).iteratedDeriv (m - 1))

The propagation step of [Kol07, 95] ("(91.1′–4′) also hold in an open neighbourhood U(p) by (55)"; [Wlo09, Lemma 5.5.3, proof, (1)]): at every point p of cosupp(I, m) there are an open neighbourhood U(p) of p and a local analytic isomorphism Φ : U(p) → M fixing p, an open embedding (onto Kollár's V(p)), such that for the pair ψ := the inclusion U(p) → M, ψ' := Φ: (1′) ψ⁻¹(H) = ψ'⁻¹(H'), (2′) ψ^*I = ψ'^*I, (3′) ψ⁻¹(E^i) = ψ'⁻¹(E^i) for every component, and (4′) ψ, ψ' agree on V(MC(ψ^*I)). The map is the coordinate swap e'⁻¹ ∘ e of exists_realizing_swap restricted to U(p); the four identities spread from the stalk at p to a neighbourhood as explained in the module docstring.