The glued blow-down of a compatible family: the isomorphism off Z and normal crossings

The blow-down σ = C.limitBlowDown Kex hemb hcomp : M̃ → M of a compatible family's direct limit (Hironaka.Resolution.Analytic.Functor.LimitFamily) is glued from the composite blow-downs Π^{(m)} : M'_m → M_m of the pieces over the members M_m = relCompactOpen Kex m of the exhaustion. Two pointwise properties of the compatible families of the main theorems glue, for any C : CompatibleFamily T:

• CompatibleFamily.isAnalyticIsoOver_limitBlowDown ([Kol07, Theorem 35, (3)]; [Wlo09, Lemma 4.0.3]): if every piece's composite blow-down is an analytic isomorphism off the trace of Z, then σ is an analytic isomorphism off Z: a local diffeomorphism at every point of σ⁻¹(Zᶜ) through the piece containing it (σ ∘ toLimit m is the piece's blow-down, toLimit m a local diffeomorphism, IsLocalDiffeomorphAt.of_comp_left), injective on σ⁻¹(Zᶜ) because two points with the same image lie in a common piece (exists_common_toLimit), where the piece's bijection decides, and onto Zᶜ because every point of M lies in some M_m (iUnion_relCompactOpen).
• CompatibleFamily.isNormalCrossingsDivisor_comap_limitBlowDown ([Kol07, Theorem 35, (2)]; [Wlo09, Theorem 2.0.3, (3)]): if over every M_m the pull-back of J|_{M_m} along the piece's composite blow-down is a normal-crossings divisor, so is J.comap σ: the condition is pointwise, and at toLimit m y the stalk of J.comap σ is carried by the germ isomorphism of the open embedding toLimitMap m onto the stalk at y of the piece's pull-back (IdealSheaf.pullback_comp, limitDesc_comp_toLimitMap, exists_monomial_of_comap_of_isLocalDiffeomorphAt).

Two general lemmas carry the transport: IsLocalDiffeomorphAt.of_comp_left (if g ∘ f and f are local diffeomorphisms at x, so is g at f x, through Mathlib's localInverse) and exists_monomial_of_comap_of_isLocalDiffeomorphAt (the pointwise normal-crossings condition descends along a local diffeomorphism at the point: the germ map is a ring isomorphism of the stalks, germMap_bijective_of_isLocalDiffeomorphAt, carrying a regular system of parameters onto one and the Krull dimension along, stalkIdeal_comap_eq_map_germMap).

theorem Hironaka.Manifold.IsLocalDiffeomorphAt.of_comp_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H₁ : Type u_5} [TopologicalSpace H₁] {H₂ : Type u_6} [TopologicalSpace H₂] {H₃ : Type u_7} [TopologicalSpace H₃] {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} {K : ModelWithCorners 𝕜 F' H₃} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H₁ M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H₂ N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace H₃ P] {n : WithTop ℕ∞} {f : M → N} {g : N → P} {x : M} (hgf : IsLocalDiffeomorphAt I K n (g ∘ f) x) (hf : IsLocalDiffeomorphAt I J n f x) : IsLocalDiffeomorphAt J K n g (f x)

If g ∘ f and f are local diffeomorphisms at x, then g is one at f x: the local inverse of f followed by the local diffeomorphism of g ∘ f (the general form behind the gluing of σ ∘ toLimit m = Π^{(m)}).

theorem Hironaka.Manifold.exists_monomial_of_comap_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (J : M.IdealSheaf) {a : N.carrier} (hh : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑h) a) (H : ∃ (k : ℕ) (z : Fin k → AnalyticManifold.IdealSheaf.stalkRing N a) (α : Fin k → ℕ), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal (AnalyticManifold.IdealSheaf.stalkRing N a) ∧ ↑k = ringKrullDim (AnalyticManifold.IdealSheaf.stalkRing N a)) ∧ (Manifold.IdealSheaf.pullback ⇑h ⋯ J).stalkIdeal a = Ideal.span {∏ i : Fin k, z i ^ α i}) : ∃ (k : ℕ) (z : Fin k → AnalyticManifold.IdealSheaf.stalkRing M (h a)) (α : Fin k → ℕ), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal (AnalyticManifold.IdealSheaf.stalkRing M (h a)) ∧ ↑k = ringKrullDim (AnalyticManifold.IdealSheaf.stalkRing M (h a))) ∧ Manifold.IdealSheaf.stalkIdeal J (h a) = Ideal.span {∏ i : Fin k, z i ^ α i}

The pointwise normal-crossings condition (record predicate at one point) descends along a local diffeomorphism at the point (gluing): the germ map is a ring isomorphism of the stalks carrying the stalk of the pull-back onto the stalk of J (stalkIdeal_comap_eq_map_germMap), a regular system of parameters onto one (the image of the maximal ideal is the maximal ideal), and the Krull dimensions agree.

theorem Hironaka.Manifold.CompatibleFamily.isAnalyticIsoOver_limitBlowDown {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} (C : CompatibleFamily T) (Kex : CompactExhaustion M.carrier) (hemb : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂), Manifold.IsAnalyticOpenEmbedding (C.endResultEmbedding hU₁ hU₂ h)) (hcomp : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) (p : ((C.seqOn U₁ hU₁).stage (Fin.last (C.seqOn U₁ hU₁).length)).carrier), (C.seqOn U₂ hU₂).toSuccession.composite ((C.endResultEmbedding hU₁ hU₂ h) p) = (M.restrictLE h) ((C.seqOn U₁ hU₁).toSuccession.composite p)) (Z : Set M.carrier) (hiso : ∀ (m : ℕ), ((C.seqOn (Manifold.relCompactOpen Kex m) ⋯).toSuccession.stageMap (Fin.last (C.seqOn (Manifold.relCompactOpen Kex m) ⋯).toSuccession.length)).IsIsoOver (Subtype.val ⁻¹' Z)ᶜ) : (C.limitBlowDown Kex hemb hcomp).IsIsoOver Zᶜ

The gluing of the isomorphism off Z ([Kol07, Theorem 35, (3)]; [Wlo09, Lemma 4.0.3]), the general form: if over every M_m the piece's composite blow-down is an analytic isomorphism off the trace of Z, then σ is an analytic isomorphism off Z — pointwise a local diffeomorphism through the piece (σ ∘ toLimit m = Π^{(m)}, IsLocalDiffeomorphAt.of_comp_left), injective on σ⁻¹(Zᶜ) through a common piece (exists_common_toLimit), onto Zᶜ through the piece over the member of the exhaustion containing the point.

theorem Hironaka.Manifold.CompatibleFamily.isNormalCrossingsDivisor_comap_limitBlowDown {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} (C : CompatibleFamily T) (Kex : CompactExhaustion M.carrier) (hemb : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂), Manifold.IsAnalyticOpenEmbedding (C.endResultEmbedding hU₁ hU₂ h)) (hcomp : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) (p : ((C.seqOn U₁ hU₁).stage (Fin.last (C.seqOn U₁ hU₁).length)).carrier), (C.seqOn U₂ hU₂).toSuccession.composite ((C.endResultEmbedding hU₁ hU₂ h) p) = (M.restrictLE h) ((C.seqOn U₁ hU₁).toSuccession.composite p)) (J : M.IdealSheaf) (hsnc : ∀ (m : ℕ), AnalyticManifold.IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑((C.seqOn (Manifold.relCompactOpen Kex m) ⋯).toSuccession.stageMap (Fin.last (C.seqOn (Manifold.relCompactOpen Kex m) ⋯).toSuccession.length)) ⋯ (Manifold.IdealSheaf.pullback ⇑(M.inclusion (Manifold.relCompactOpen Kex m)) ⋯ J))) : AnalyticManifold.IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑(C.limitBlowDown Kex hemb hcomp) ⋯ J)

The gluing of the normal-crossings clause ([Kol07, Theorem 35, (2)]; [Wlo09, Theorem 2.0.3, (3)]), the general form: if over every M_m the pull-back of J|_{M_m} along the piece's composite blow-down is a normal-crossings divisor, so is the pull-back of J along σ — the condition is pointwise, and at toLimit m y the stalk of J.pullback σ σ.contMDiff is carried onto the stalk at y of the piece's pull-back by the germ isomorphism of toLimitMap m (σ ∘ toLimitMap m = Π^{(m)} after the inclusion of M_m, IdealSheaf.pullback_comp).