The first step of Lemma 102 under pull-back

The proof of [Kol07, Lemma 102] checks that the construction commutes with smooth morphisms h : Y → X: the restriction h|_{E^j_Y} : E^j_Y → E^j "is also a smooth surjection", and pulling back by h and then restricting to E^j_Y gives the same result as restricting to E^j and then pulling back by h|_{E^j_Y}. This module proves the corresponding facts for a local analytic isomorphism h : N → M and the first step of the construction (FirstStep.lean):

• Zminus1_comap — the first centre of the pulled-back data (h^* 𝓘, h⁻¹(E^j)) is the preimage of the first centre: a connected component of h⁻¹(E^j) lies in cosupp(h^* 𝓘, m) iff the component of E^j it maps into lies in cosupp(𝓘, m). Kollár argues at the generic point; here the identity theorem on the connected hypersurface stands in: the order of 𝓘 along E^j is constant on a component (ordAlong_eq_of_isPreconnected), it is at least m at h x when ord 𝓘 ≥ m on the open piece h(component of x) of E^j near h x (a local analytic isomorphism is an open map), and ord_{E^j} 𝓘 ≤ ord 𝓘 pointwise. No surjectivity is needed.
• firstStep_pullback — the one-step sequence blowing up Z_{-1} pulls back to the one-step sequence blowing up the first centre of the pulled-back data.
• isLocalDiffeomorph_restrictMap, surjective_restrictMap — the restriction h⁻¹(S) → S of h to the preimage of a closed hypersurface is a local analytic isomorphism between the bundled hypersurfaces (the local inverses of h restrict), and a surjection when h is.
• pullback_inclusionMap_pullback, comap_inclusionMap_comap — restriction and pull-back commute, for the ideal sheaf (the pull-back of ideal sheaves is functorial) and for the boundary family (componentwise, the index set kept).

These are the ingredients of the commutation of Lemma 102's functor with local analytic isomorphisms ([Kol07, Lemma 102 (2)]), assembled in BDOf.lean (and BDErase.lean).

The first centre of the pulled-back data

theorem Hironaka.Manifold.BD.Zminus1_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (I : M.IdealSheaf) (m : ℕ) {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ₀ Y 1) : Zminus1 (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m (⇑h ⁻¹' Y) = ⇑h ⁻¹' Zminus1 I m Y

The first centre of the pulled-back data is the preimage of the first centre (the functoriality part of the proof of [Kol07, Lemma 102], with the identity theorem on the connected hypersurface in place of Kollár's generic-point argument): a connected component of h⁻¹(E^j) lies in cosupp(h^* 𝓘, m) iff the component of E^j it maps into lies in cosupp(𝓘, m). The component maps into the component by continuity; conversely, ord 𝓘 ≥ m on the open piece of E^j that is the image of the component near h x forces ord_{E^j} 𝓘 ≥ m at h x, hence along the whole connected component of h x (the order along E^j is locally constant), hence ord 𝓘 ≥ m there.

theorem Hironaka.Manifold.BD.firstStep_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (I : M.IdealSheaf) (m : ℕ) {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ₀ Y 1) (hZ : Manifold.IsClosedSubmanifold ψ₀ (Zminus1 I m Y) 1) (hZ' : Manifold.IsClosedSubmanifold ψ₀ (Zminus1 (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m (⇑h ⁻¹' Y)) 1) : (AnalyticManifold.BlowUpSequence.cons hZ (AnalyticManifold.BlowUpSequence.nil (Manifold.blowUp ψ₀ hZ))).pullback h hh = AnalyticManifold.BlowUpSequence.cons hZ' (AnalyticManifold.BlowUpSequence.nil (Manifold.blowUp ψ₀ hZ'))

The one-step sequence blowing up Z_{-1} pulls back along a local analytic isomorphism to the one-step sequence blowing up the first centre of the pulled-back data (BlowUpSequence.pullback_cons and Zminus1_comap, the two centres being the same set).

The restriction of a local analytic isomorphism to the preimage of a hypersurface

noncomputable def Hironaka.Manifold.BD.restrictInvFunOfPreimage {𝕜 : 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) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΨ : Set.EqOn (⇑h) (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : ⋯.toAnalyticManifold.carrier) (y : hS.toAnalyticManifold.carrier) : ⋯.toAnalyticManifold.carrier

The local inverse Ψ of h read on the bundled hypersurfaces: Ψ⁻¹(y) for y ∈ S ∩ Ψ.target, which lies in h⁻¹(S) since h (Ψ⁻¹ y) = y; a default value p₀ elsewhere. An auxiliary construction for restrictPartialDiffeomorphOfPreimage.

Equations

• Hironaka.Manifold.BD.restrictInvFunOfPreimage h hh hS Ψ hΨ p₀ y = if hy : ↑y ∈ Ψ.target then ⟨Ψ.invFun ↑y, ⋯⟩ else p₀

theorem Hironaka.Manifold.BD.restrictInvFunOfPreimage_of_mem {𝕜 : 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) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΨ : Set.EqOn (⇑h) (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : ⋯.toAnalyticManifold.carrier) {y : hS.toAnalyticManifold.carrier} (hy : ↑y ∈ Ψ.target) : restrictInvFunOfPreimage h hh hS Ψ hΨ p₀ y = ⟨Ψ.invFun ↑y, ⋯⟩

The value of restrictInvFunOfPreimage on the target of Ψ.

noncomputable def Hironaka.Manifold.BD.restrictPartialDiffeomorphOfPreimage {𝕜 : 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) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΨ : Set.EqOn (⇑h) (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : ⋯.toAnalyticManifold.carrier) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤

A local inverse of h restricted to the bundled hypersurfaces h⁻¹(S) and S is a partial diffeomorphism agreeing with the restricted map on h⁻¹(S) ∩ Ψ.source.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BD.isLocalDiffeomorph_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - 1) → 𝕜)) ⊤ ⇑(⋯.restrictMap hS ⇑h ⋯ ⋯)

"h|_{E^j_Y} : E^j_Y → E^j is also a smooth surjection" (the proof of [Kol07, Lemma 102]), the local-isomorphism part: the restriction of a local analytic isomorphism to the preimage of a closed hypersurface is a local analytic isomorphism between the bundled hypersurfaces, the local inverses of h restricting to the submanifolds.

theorem Hironaka.Manifold.BD.surjective_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hs : Function.Surjective ⇑h) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (hS' : Manifold.IsClosedSubmanifold ψ₀ (⇑h ⁻¹' S) 1) : Function.Surjective ⇑(hS'.restrictMap hS ⇑h ⋯ ⋯)

The restriction of a surjection to the preimage of a hypersurface is a surjection onto the hypersurface (true for every analytic map).

Restriction and pull-back commute

theorem Hironaka.Manifold.BD.pullback_inclusionMap_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (I : M.IdealSheaf) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (hS' : Manifold.IsClosedSubmanifold ψ₀ (⇑h ⁻¹' S) 1) : Manifold.IdealSheaf.pullback ⇑hS'.inclusionMap ⋯ (Manifold.IdealSheaf.pullback ⇑h ⋯ I) = Manifold.IdealSheaf.pullback ⇑(hS'.restrictMap hS ⇑h ⋯ ⋯) ⋯ (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ I)

Pulling back by h and then restricting to E^j_Y gives "the same result" as restricting to E^j and then pulling back by h|_{E^j_Y} (the proof of [Kol07, Lemma 102]), for the ideal sheaf: the restriction to h⁻¹(S) of the pull-back of 𝓘 is the pull-back along h|_{h⁻¹(S)} of the restriction of 𝓘 to S, because the pull-back of ideal sheaves is functorial and ι_S ∘ h|_{h⁻¹(S)} = h ∘ ι_{h⁻¹(S)}.

theorem Hironaka.Manifold.BD.comap_inclusionMap_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (F : Manifold.HypersurfaceFamily M.carrier) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S 1) (hS' : Manifold.IsClosedSubmanifold ψ₀ (⇑h ⁻¹' S) 1) : Manifold.HypersurfaceFamily.comap (⇑hS'.inclusionMap) (Manifold.HypersurfaceFamily.comap (⇑h) F) = Manifold.HypersurfaceFamily.comap (⇑(hS'.restrictMap hS ⇑h ⋯ ⋯)) (Manifold.HypersurfaceFamily.comap (⇑hS.inclusionMap) F)

The same for the boundary (E − E^j)|_{E^j}: the restriction to h⁻¹(S) of the pulled-back family is the pull-back along h|_{h⁻¹(S)} of the restricted family (componentwise, the index set kept; true for every map).