Uniqueness of maximal contact in local-isomorphism form

The covering step of Kollár's proof of the uniqueness of maximal contact [Kol07, 95]: "the images of finitely many of the U(p) cover X; we can take U to be their disjoint union". On a second countable analytic manifold, countably many of the neighbourhoods U(p) of locallyIsoEquivalent_on_nhd (Hironaka/Resolution/Analytic/MaximalContact/Propagation.lean) cover cosupp(I, m) (TopologicalSpace.countable_cover_nhdsWithin), and their disjoint union U := ∐ U(p) (sigmaManifold) carries the two local analytic isomorphisms ψ := ∐ (inclusions) and ψ' := ∐ Φ(p) (ContMDiff.sigmaDesc, IsLocalDiffeomorph.sigmaDesc). Their images contain cosupp(I, m): for ψ by the cover, for ψ' because Φ(p) fixes every point of cosupp(I, m) ∩ U(p) — such a point lies on V(MC(I)), where (4′) forces ψ' = ψ (the order of MC(I) = D^{m−1}I there is 1, ord_iteratedDeriv_eq_one).

Conditions (1′)–(4′) of [Kol07, Definition 91] descend from the summands: (1′) and (3′) are pointwise; for (2′) and (4′) the stalk map of the summand inclusion σ_t : U(t) → ∐ U(p) is bijective — because ψ ∘ σ_t = ι_{U(t)} and both ψ and the inclusion have bijective stalk maps (germMap_val_bijective, germMap_bijective_of_isLocalDiffeomorphAt) — so the stalks of ψ^*I, ψ'^*I and of MC(ψ^*I) at σ_t x are read off from the stalks on U(t) through Ideal.comap_map_of_bijective, where (2′) and (4′) hold.

The result (maximalContact_locallyIsoEquivalent) is Kollár's uniqueness of maximal contact [Kol07, Theorem 92] on analytic manifolds, with local analytic isomorphisms in place of étale surjections; it feeds the independence of the order-reduction algorithm from the choice of the hypersurface of maximal contact (Hironaka/Resolution/Analytic/OrderReduction/FamilyIndependence.lean).

theorem Hironaka.Manifold.germMap_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N P : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (g : AnalyticMap P N) (x : P.carrier) : (Manifold.germMap ⇑g ⋯ x).comp (Manifold.germMap ⇑f ⋯ (g x)) = Manifold.germMap ⇑(ContMDiffMap.comp f g) ⋯ x

The stalk map of a composite of analytic maps is the composite of the stalk maps (germMapOn_germMapOn, bundled).

theorem Hironaka.Manifold.maximalContact_locallyIsoEquivalent {𝕜 : 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) (hmax : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) (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')) : Nonempty (LocallyIsoEquivalentMC I m F H H')

Uniqueness of maximal contact in local-isomorphism form ([Kol07, Theorem 92], through the covering step of [Kol07, 95]): for I MC-invariant with ord I ≤ m everywhere, m ≥ 1, E snc, and H, H' smooth hypersurfaces of maximal contact for I (their ideal sheaves contained in MC(I) = D^{m−1}(I)) such that H + E and H' + E both have simple normal crossings, H and H' are local-isomorphism equivalent with respect to (M, I, E): countably many of the neighbourhoods U(p) of locallyIsoEquivalent_on_nhd cover cosupp(I, m), and on their disjoint union ∐ U(p) the pair (∐ inclusions, ∐ Φ(p)) satisfies (1′)–(4′) summand by summand.