Transport of normal crossings along a diffeomorphism

Hironaka's normal crossings [Hir64, Definition 2] at the stalk level (AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith) is stated through a regular system of parameters of the stalk, the minimal primes of the divisor's stalk and generators of the centre's stalk. All three transport along a ring isomorphism of the stalks, here the germ map of a diffeomorphism g : M₁ ≃ M₂ at a point (germMap, bijective by germMap_bijective_of_isLocalDiffeomorphAt): the pull-backs g^* E, g^* D have only normal crossings when E, D have. This is the piece of the normal-crossings clause of the push-forward that concerns the identification T_i ≃ S_i of the stages of a sequence with those of the restricted push-forward ([Kol07, 30.2–30.3]).

• Ideal.comap_mem_minimalPrimes_of_bijective: minimal primes over J S pull back to minimal primes over J along a bijective ring map.
• AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith.pullback_diffeomorph: the transport itself.

theorem Ideal.comap_mem_minimalPrimes_of_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (e : R →+* S) (he : Function.Bijective ⇑e) {J : Ideal R} {P : Ideal S} (hP : P ∈ (map e J).minimalPrimes) : comap e P ∈ J.minimalPrimes

A minimal prime over the extension J S of an ideal along a bijective ring map pulls back to a minimal prime over J.

theorem AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith.pullback_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁ M₂ : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁.carrier M₂.carrier ⊤) {E' D : M₂.IdealSheaf} (h : E'.HasOnlyNormalCrossingsWith D) : HasOnlyNormalCrossingsWith (Manifold.IdealSheaf.pullback ⇑g ⋯ E') (Manifold.IdealSheaf.pullback ⇑g ⋯ D)

Hironaka's normal crossings [Hir64, Definition 2] at the stalk level transport along a diffeomorphism: for g : M₁ ≃ M₂ and ideal sheaves E', D on M₂ with E' having only normal crossings with D, the pull-backs have only normal crossings; the regular system of parameters, the minimal primes and the generators of the centre are carried by the (bijective, local) germ map of g at the point.