The pull-back of a reduced ideal sheaf along a local analytic isomorphism

A local analytic isomorphism φ : N → M has bijective germ maps at every point (germMap_bijective_of_isLocalDiffeomorphAt), so the stalk of the pull-back φ^*J at b is the image of the stalk of J at φ b under a ring isomorphism; a radical ideal maps to a radical ideal, and φ^*J is reduced when J is (IdealSheaf.isReduced_pullback_of_isLocalDiffeomorph). This is the local-isomorphism counterpart of IdealSheaf.isReduced_pullback_diffeomorph, and the reason the pairs (M, Y) of a manifold and a reduced closed subspace pull back along local analytic isomorphisms (AnalyticManifold.EmbeddedPair.pullback).

theorem Manifold.IdealSheaf.isReduced_pullback_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (φ : AnalyticMap N M) (hφ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑φ) {J : M.IdealSheaf} (hJ : J.IsReduced) : AnalyticManifold.IdealSheaf.IsReduced (pullback ⇑φ ⋯ J)

The pull-back of a reduced ideal sheaf along a local analytic isomorphism is reduced: the germ maps of a local analytic isomorphism are ring isomorphisms at every point (germMap_bijective_of_isLocalDiffeomorphAt), and a radical ideal maps to a radical ideal under a surjective ring homomorphism with trivial kernel.