The vanishing stalk of a preimage along a local analytic isomorphism, for charted types

vanishingStalk_preimage_of_isLocalDiffeomorphAt of Hironaka/Resolution/Analytic/Functor/PullbackTransport.lean is stated for bundled analytic manifolds and an AnalyticMap; here the same statements are proved for a bare analytic map between charted types ([IsManifold 𝓘(𝕜, E) ω M] alone, no Hausdorff or second-countability assumptions): a germ vanishes on h⁻¹(Z) at b iff its push-forward along the local inverse vanishes on Z at h b (Germ.vanishesOn_compTendsto_of_isLocalDiffeomorphAt'), and vanishingStalk (h ⁻¹' Z) b = Ideal.map (germMap h hh b) (vanishingStalk Z (h b)) (vanishingStalk_preimage_of_isLocalDiffeomorphAt', through the bijective germ map germMap_bijective_of_isLocalDiffeomorphAt). The proofs are those of the bundled lemmas. Off the centre of a blowing-up the map is a local analytic isomorphism (condition (1) of [BM88, Definition 4.1]) and the strict transforms are the preimages of the components, so the vanishing stalks upstairs are transports of the vanishing stalks downstairs; this is used in the Jacobian bookkeeping of the Hironaka library (Hironaka/Resolution/Analytic/BM97/LedgerStep.lean, Hironaka/Resolution/Analytic/ModelTransport/Square.lean).

theorem Hironaka.Manifold.Germ.vanishesOn_compTendsto_of_isLocalDiffeomorphAt' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {h : N → M} (hh : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h) {b : N} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h b) (Z : Set M) (k : (nhds (h b)).Germ 𝕜) : Manifold.Germ.VanishesOn (h ⁻¹' Z) b (k.compTendsto h ⋯) ↔ Manifold.Germ.VanishesOn Z (h b) k

A germ at h b vanishes on Z iff its pull-back along the local analytic isomorphism h vanishes on h⁻¹(Z) at b (the charted-type form of Germ.vanishesOn_compTendsto_of_isLocalDiffeomorphAt): near b the map h agrees with a partial diffeomorphism Φ, which carries 𝓝[h ⁻¹' Z] b onto 𝓝[Z] (h b).

theorem Hironaka.Manifold.vanishingStalk_preimage_of_isLocalDiffeomorphAt' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {h : N → M} (hh : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h) {b : N} (hb : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h b) (Z : Set M) : Manifold.vanishingStalk (h ⁻¹' Z) b = Ideal.map (Manifold.germMap h hh b) (Manifold.vanishingStalk Z (h b))

The vanishing stalk of h⁻¹(Z) at b is the image of the vanishing stalk of Z at h b under the germ map of the local analytic isomorphism h at b (the charted-type form of vanishingStalk_preimage_of_isLocalDiffeomorphAt, for a bare analytic map between charted types): the comap of the vanishing stalk of the preimage is the vanishing stalk of Z (the germ identity above), and Ideal.map of a comap along a surjection is the ideal itself (germMap_bijective_of_isLocalDiffeomorphAt).