The monomial and nonmonomial parts commute with local analytic isomorphisms

For a local analytic isomorphism h : N → M and a boundary family F on M with simple normal crossings, the pulled-back family F.comap h has the members h⁻¹(E^j), and the monomial part with respect to it of the pulled-back ideal is the pull-back of the monomial part: M(h^*𝓘) = h^* M(𝓘), and likewise N(h^*𝓘) = h^* N(𝓘) (monomialPart_comap, nonmonomialPart_comap). This is the compatibility of the decomposition 𝓘 = M(𝓘) · N(𝓘) of [Kol07, Definition–Lemma 110] with local analytic isomorphisms, the analytic form of the smooth morphisms of [Kol07, 34.1], which the functoriality of the marked order reduction [Kol07, Theorem 107 (2)] requires of every step of its construction.

Since M(𝓘) is a locally finite product of component factors (BMO/MonomialPart.lean), the statement is proved stalk by stalk. Its core is the correspondence of connected components under h: at a point b with a = h b, the connected component of h⁻¹(E^j) through b agrees near b with the preimage of the component of E^j through a (both agree with h⁻¹(E^j) near b, the components being open in their members), so the two reduced ideal sheaves have the same stalk (componentIdeal_comap_stalkIdeal), and the order of h^*𝓘 along the one is the order of 𝓘 along the other (componentExponent_comap). The factors through b then correspond bijectively to the factors through a, with equal exponents.

theorem Hironaka.Manifold.BMO.map_finset_prod_ideal {R : Type u_2} {S : Type u_3} {F : Type u_4} [CommRing R] [CommRing S] [FunLike F R S] [RingHomClass F R S] (f : F) {ι : Type u_5} (s : Finset ι) (J : ι → Ideal R) : Ideal.map f (∏ i ∈ s, J i) = ∏ i ∈ s, Ideal.map f (J i)

Ideal.map along a ring homomorphism distributes over a finite product of ideals.

theorem Hironaka.Manifold.BMO.exists_isOpen_componentSet_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily M.carrier) (hG : Manifold.HypersurfaceFamily.IsSnc ψ₀ G) (i₀ : ComponentIndex G) : ∃ (W : Set M.carrier), IsOpen W ∧ componentSet G i₀ = G.hyp i₀.fst ∩ W

A connected component of a member of a boundary family with simple normal crossings is the intersection of the member with an open set of M: the member is a closed submanifold, hence locally connected, so its connected components are open in it.

theorem Hironaka.Manifold.BMO.mem_componentSet_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily M.carrier) (j : G.ι) {x : M.carrier} (hx : x ∈ G.hyp j) : x ∈ componentSet G ⟨j, ConnectedComponents.mk ⟨x, hx⟩⟩

A point of a member lies on the component indexed by its own connected component.

theorem Hironaka.Manifold.BMO.mk_eq_of_mem_componentSet {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily M.carrier) (i₀ : ComponentIndex G) {x : M.carrier} (hx : x ∈ componentSet G i₀) (hxmem : x ∈ G.hyp i₀.fst) : ConnectedComponents.mk ⟨x, hxmem⟩ = i₀.snd

The connected component of a point of componentSet G i₀ in its member is the component of i₀.

theorem Hironaka.Manifold.BMO.componentIndex_ext_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {G : Manifold.HypersurfaceFamily M.carrier} {i₁ i₂ : ComponentIndex G} {x : M.carrier} (h1 : x ∈ componentSet G i₁) (h2 : x ∈ componentSet G i₂) (hj : i₁.fst = i₂.fst) : i₁ = i₂

Two components of G through a common point x with the same member index are equal: each is the connected component of x in that member.

theorem Hironaka.Manifold.BMO.componentIdeal_comap_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (i : ComponentIndex F) (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap (⇑h) F)) {b : N.carrier} (hib : b ∈ componentSet (Manifold.HypersurfaceFamily.comap (⇑h) F) i') (hnb : h b ∈ componentSet F i) (hji : i'.fst = i.fst) : (componentIdeal (Manifold.HypersurfaceFamily.comap (⇑h) F) ⋯ i').stalkIdeal b = (Manifold.IdealSheaf.pullback ⇑h ⋯ (componentIdeal F hF i)).stalkIdeal b

Let i' be a component of the pulled-back family F.comap h and i a component of F with the same member index, and let b lie on i' with h b on i. Then the stalk at b of the reduced ideal sheaf of i' is the stalk of the pull-back h^* 𝓘_D of the reduced ideal sheaf of i: the component i' and the preimage h⁻¹(D) agree on a neighbourhood of b, both being the member h⁻¹(E^j) there (exists_isOpen_componentSet_eq on either side), and the ideal sheaf of a closed submanifold depends only on the submanifold near the point.

theorem Hironaka.Manifold.BMO.componentExponent_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (I : M.IdealSheaf) (i : ComponentIndex F) (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap (⇑h) F)) {b : N.carrier} (hib : b ∈ componentSet (Manifold.HypersurfaceFamily.comap (⇑h) F) i') (hnb : h b ∈ componentSet F i) (hji : i'.fst = i.fst) : componentExponent (Manifold.HypersurfaceFamily.comap (⇑h) F) ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ I) i' = componentExponent F hF I i

The exponents of the monomial part transport under a local analytic isomorphism: for a component i' of F.comap h and the component i of F with the same member index that h maps it into, ord_{D'}(h^*𝓘) = ord_D 𝓘. The order along a component is read at any of its points; at b the two reduced ideal sheaves agree (componentIdeal_comap_stalkIdeal) and the order along a submanifold is preserved by a local analytic isomorphism.

theorem Hironaka.Manifold.BMO.componentFactor_comap_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (I : M.IdealSheaf) (i : ComponentIndex F) (i' : ComponentIndex (Manifold.HypersurfaceFamily.comap (⇑h) F)) {b : N.carrier} (hib : b ∈ componentSet (Manifold.HypersurfaceFamily.comap (⇑h) F) i') (hnb : h b ∈ componentSet F i) (hji : i'.fst = i.fst) : (componentFactor (Manifold.HypersurfaceFamily.comap (⇑h) F) ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ I) i').stalkIdeal b = Ideal.map (germAlgEquiv h ⋯) ((componentFactor F hF I i).stalkIdeal (h b))

The factor of M(h^*𝓘) at a component i' of F.comap h, at a stalk b, is the image of the factor of M(𝓘) at the corresponding component i of F under the isomorphism of stalks induced by h: the two reduced ideal sheaves correspond (componentIdeal_comap_stalkIdeal) and the exponents agree (componentExponent_comap).

theorem Hironaka.Manifold.BMO.monomialPart_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (I : M.IdealSheaf) : monomialPart (Manifold.HypersurfaceFamily.comap (⇑h) F) ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ I) = Manifold.IdealSheaf.pullback ⇑h ⋯ (monomialPart F hF I)

The monomial part commutes with pull-back along a local analytic isomorphism: M(h^*𝓘) = h^* M(𝓘), the monomial part on the left taken with respect to the pulled-back boundary family F.comap h (the compatibility of [Kol07, Definition–Lemma 110] with local analytic isomorphisms, the analytic form of the smooth morphisms of [Kol07, 34.1]). Stalkwise, the components of F.comap h through b correspond bijectively to the components of F through h b, with corresponding factors (componentFactor_comap_stalkIdeal).

theorem Hironaka.Manifold.BMO.nonmonomialPart_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (I : M.IdealSheaf) : nonmonomialPart (Manifold.HypersurfaceFamily.comap (⇑h) F) ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ I) = Manifold.IdealSheaf.pullback ⇑h ⋯ (nonmonomialPart F hF I)

The nonmonomial part commutes with pull-back along a local analytic isomorphism: N(h^*𝓘) = h^* N(𝓘). The colon 𝓘 : M(𝓘) transports under the isomorphism of stalks induced by h, and the monomial part transports by monomialPart_comap. This is the ideal half of the statement that the nonmonomial triple of a pulled-back triple is the pull-back of the nonmonomial triple (Modified/NonmonomialComapInhabit.lean).