A compatible family over the re-modelled manifold, read back on the manifold

Włodarczyk's compatible family of finite successions (ExtensionCompatibleFamily; [Wlo09, Theorem 2.0.3 (1), (4); Definition 3.2.6]) constructed over the re-modelled manifold M.transport ψ (in the analytic main theorems the standard model Fin n → ℝ, where the resolution resolveFam lives) is read back on M (transportBack): the space re-modelled along ψ⁻¹, the same map and the same neighbourhoods, each succession carried along the identity of its neighbourhood (transportAlong of Succession.lean at the stage-0 identification restrictTransportDiffeomorph), the identification of the end results conjugated by the identities, and the compatibility by isExtensionOf_restrict_transportAlong (SuccessionExtension.lean). Every clause of the two manifold-level main theorems (Hironaka's Main Theorem II''(N) and the real-analytic principalization with the Jacobian clause, at the ends of Hironaka/Resolution/Analytic/Wlo09/HironakaAssembly.lean and Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean) then transports, word for word:

• the map: properness (isProperMap_map_transportBack_iff, definitional), the divisor clause on J.comap map (isNormalCrossingsDivisor_comap_map_transportBack_iff), the Jacobian clause (isNormalCrossingsDivisor_jacobianIdeal_mul_pullback_map_transportBack_iff: jacobianIdeal_of_square on the square of F.map with the two identities — the Jacobian ideal of the transported map is the pull-back of the Jacobian ideal, no unit germ) and the isomorphism off the cosupport (isAnalyticIsoOver_map_transportBack_iff);
• per compact: the centres are non-singular (isNonsingular_center_seq_transportBack_iff), the boundaries have only normal crossings with the centres (the stalk-local forms hasOnlyNormalCrossingsWith_boundarySeq_center_seq_transportBack_iff, hasOnlyNormalCrossings_boundarySeq_last_seq_transportBack_iff, kept as general tools), the last weak transform is the unit ideal (weakTransformSeq_last_seq_transportBack_eq_unit_iff), the order of a weak transform at a point (ord_weakTransformSeq_seq_transportBack) and the support of a centre (support_center_seq_transportBack) — all through the pull-back identities center_seq_transportBack, weakTransformSeq_seq_transportBack, boundarySeq_seq_transportBack (the identities of Succession.lean with the restriction of the re-modelled sheaves, restrictOpens_eq_pullbackDiffeomorph_transport) and the predicate transports of Hironaka/Resolution/Analytic/ModelTransport/IdealSheaf.lean;
• the boundary clauses in the simple-normal-crossings family form: for fixed chart isomorphisms on the two models (exists_isSnc_boundarySeq_hasSncWith_center_seq_transportBack_iff, exists_isSnc_boundarySeq_last_seq_transportBack_iff, from SncFamily.lean along the stage identification) and in the predicates IsSncBoundaryWith/IsSncBoundary of the main theorems (isSncBoundaryWith_boundarySeq_center_seq_transportBack_iff, isSncBoundary_boundarySeq_last_seq_transportBack_iff, at the model isomorphism ψ⁻¹), the forms the proofs of the main theorems read;
• Włodarczyk's embedded desingularization ([Wlo09, Theorem 2.0.2]): the strict transforms of a closed subspace (strictTransformSubspaceSeq_seq_transportBack), the isomorphism off its singular locus (isAnalyticIsoOver_compl_sing_map_transportBack_iff), and all its clauses on the succession over a compact at once (isDesingularizedBy_seq_transportBack), and its divisor and strict transform on the glued space (IdealSheaf.IsGloballyDesingularizedBy, the clause exists_divisor_strictTransform of IdealSheaf.IsLocallyFinitelyDesingularizedBy as a structure, defined here; isGloballyDesingularizedBy_transportBack).

The divisor and the strict transform of an embedded desingularization on M̃

structure AnalyticManifold.IdealSheaf.IsGloballyDesingularizedBy {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (F : M.ExtensionCompatibleFamily) : F.space.IdealSheaf → (Y : F.space.IdealSheaf) → Prop

The ideal sheaves E and Ỹ on the space M̃ of the compatible family F are the exceptional divisor and the strict transform of an embedded desingularization of the closed subspace Y of M with ideal sheaf I by F [Wlo09, Theorem 2.0.2]: with res_{Y,M} = F.map : M̃ → M, E is the reduced ideal sheaf of a simple normal crossings family of hypersurfaces of M̃ with which Ỹ has simple normal crossings, transversally; res_{Y,M}^*(I_Y) = I_Ỹ · I_Ẽ with Ẽ near every point an effective combination of the components of E; and over the neighbourhood U_K of every compact K ⊆ M, read through the identification toSpace K of the last stage U_r of the succession F.seq K with res_{Y,M}⁻¹(U_K), E is the last exceptional divisor E_r and Ỹ the last strict transform Y_r of Y ∩ U_K. The clause exists_divisor_strictTransform of IsLocallyFinitelyDesingularizedBy as a structure (isGloballyDesingularizedBy_iff_and).

• isSncBoundaryTransversalTo : E.IsSncBoundaryTransversalTo Y

  (1), (3) E is the reduced ideal sheaf of a simple normal crossings hypersurface family, with which Ỹ has simple normal crossings, transversally.

• isMulBoundaryMonomial : IsMulBoundaryMonomial (Manifold.IdealSheaf.pullback ⇑F.map ⋯ I) Y E

  (6) res_{Y,M}^*(I_Y) = I_Ỹ · I_Ẽ, Ẽ a combination of the components of E near every point.

• pullback_toSpace_eq_boundarySeq (K : TopologicalSpace.Compacts M.carrier) : Manifold.IdealSheaf.pullback ⇑(F.toSpace K) ⋯ E = (F.seq K).boundarySeq ⊤ (Fin.last (F.seq K).length)

  Over every compact K, E read on the last stage U_r of the succession over U_K is the last exceptional divisor E_r.

• pullback_toSpace_eq_strictTransform (K : TopologicalSpace.Compacts M.carrier) : Manifold.IdealSheaf.pullback ⇑(F.toSpace K) ⋯ Y = (F.seq K).strictTransformSubspaceSeq (I.restrict (F.nhd K)) (Fin.last (F.seq K).length)

  Over every compact K, Ỹ read on the last stage U_r of the succession over U_K is the last strict transform Y_r of Y ∩ U_K.

theorem AnalyticManifold.IdealSheaf.isGloballyDesingularizedBy_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (F : M.ExtensionCompatibleFamily) (E✝ Y : F.space.IdealSheaf) : I.IsGloballyDesingularizedBy F E✝ Y ↔ E✝.IsSncBoundaryTransversalTo Y ∧ IsMulBoundaryMonomial (Manifold.IdealSheaf.pullback ⇑F.map ⋯ I) Y E✝ ∧ (∀ (K : TopologicalSpace.Compacts M.carrier), Manifold.IdealSheaf.pullback ⇑(F.toSpace K) ⋯ E✝ = (F.seq K).boundarySeq ⊤ (Fin.last (F.seq K).length)) ∧ ∀ (K : TopologicalSpace.Compacts M.carrier), Manifold.IdealSheaf.pullback ⇑(F.toSpace K) ⋯ Y = (F.seq K).strictTransformSubspaceSeq (I.restrict (F.nhd K)) (Fin.last (F.seq K).length)

theorem AnalyticManifold.IdealSheaf.isGloballyDesingularizedBy_iff_and {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {F : M.ExtensionCompatibleFamily} {E✝ Y : F.space.IdealSheaf} : I.IsGloballyDesingularizedBy F E✝ Y ↔ (∀ (K : TopologicalSpace.Compacts M.carrier), Manifold.IdealSheaf.pullback ⇑(F.toSpace K) ⋯ E✝ = (F.seq K).boundarySeq ⊤ (Fin.last (F.seq K).length) ∧ Manifold.IdealSheaf.pullback ⇑(F.toSpace K) ⋯ Y = (F.seq K).strictTransformSubspaceSeq (I.restrict (F.nhd K)) (Fin.last (F.seq K).length)) ∧ E✝.IsSncBoundaryTransversalTo Y ∧ IsMulBoundaryMonomial (Manifold.IdealSheaf.pullback ⇑F.map ⋯ I) Y E✝

IsGloballyDesingularizedBy is the conjunction of the clause exists_divisor_strictTransform of IsLocallyFinitelyDesingularizedBy, in its order: the identifications over the compacts, then (1), (3) and (6) on M̃.

theorem AnalyticManifold.IdealSheaf.IsLocallyFinitelyDesingularizedBy.exists_isGloballyDesingularizedBy {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {F : M.ExtensionCompatibleFamily} (h : I.IsLocallyFinitelyDesingularizedBy F) : ∃ (E_1 : F.space.IdealSheaf) (Y : F.space.IdealSheaf), I.IsGloballyDesingularizedBy F E_1 Y

A locally finite embedded desingularization has a divisor and a strict transform on M̃ (IsGloballyDesingularizedBy).

Helpers on the re-modelled base

theorem AnalyticManifold.IdealSheaf.restrictOpens_eq_pullbackDiffeomorph_transport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (J : M.IdealSheaf) (U : TopologicalSpace.Opens M.carrier) : J.restrict U = pullbackDiffeomorph (M.restrictTransportDiffeomorph ψ U) ((transport ψ J).restrict (M.transportOpens ψ U))

An ideal sheaf restricted to an open, read through the stage-0 identification of the transport: the restriction of J is the pull-back of the restriction of the re-modelled J (every map in sight is the identity on points).

theorem AnalyticManifold.IdealSheaf.preimage_support_transport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (J : M.IdealSheaf) : ⇑(M.transportDiffeomorph ψ) ⁻¹' Manifold.IdealSheaf.support (transport ψ J) = Manifold.IdealSheaf.support J

The support of the re-modelled ideal sheaf, read back on M.

theorem AnalyticManifold.IdealSheaf.preimage_regularLocus_transport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (J : M.IdealSheaf) : ⇑(M.transportDiffeomorph ψ) ⁻¹' (transport ψ J).regularLocus = J.regularLocus

The simple locus of the re-modelled ideal sheaf, read back on M.

The family read back on M

noncomputable def AnalyticManifold.ExtensionCompatibleFamily.transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) : M.ExtensionCompatibleFamily

A compatible family over the re-modelled M, read back on M: the space re-modelled along ψ⁻¹, the same map and neighbourhoods, each succession carried along the identity of its neighbourhood (transportAlong), the identification of the end results conjugated by the identities; map_toSpace by composite_transportAlong, toSpace_isIso by isAnalyticIsoOver_of_square_iff on the square of the identities, the compatibility by isExtensionOf_restrict_transportAlong.

Equations

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

theorem AnalyticManifold.ExtensionCompatibleFamily.coe_map_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) : ⇑(transportBack ψ F).map = ⇑F.map ∘ ⇑(F.space.transportDiffeomorph ψ.symm).symm

The transported map is the map after the identity of the space.

theorem AnalyticManifold.ExtensionCompatibleFamily.nhd_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) : (transportBack ψ F).nhd K = F.nhd K

The same neighbourhoods.

theorem AnalyticManifold.ExtensionCompatibleFamily.seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) : (transportBack ψ F).seq K = FiniteSuccession.transportAlong (M.restrictTransportDiffeomorph ψ (F.nhd K)) ψ.symm (F.seq K)

The succession of K, carried along the identity of U_K.

theorem AnalyticManifold.ExtensionCompatibleFamily.coe_toSpace_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) : ⇑((transportBack ψ F).toSpace K) = ⇑(F.space.transportDiffeomorph ψ.symm) ∘ ⇑(F.toSpace K) ∘ ⇑(FiniteSuccession.transportAlongStage (M.restrictTransportDiffeomorph ψ (F.nhd K)) ψ.symm (F.seq K) (Fin.last (F.seq K).length))

The identification of the end result, conjugated by the identities.

theorem AnalyticManifold.ExtensionCompatibleFamily.isProperMap_map_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) : IsProperMap ⇑(transportBack ψ F).map ↔ IsProperMap ⇑F.map

Properness of the transported map: the same map on the same topologies, definitionally.

The per-compact clauses

@[reducible, inline]

noncomputable abbrev AnalyticManifold.ExtensionCompatibleFamily.stageEquiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((F.seq K).length + 1)) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (((transportBack ψ F).seq K).stage i).carrier ((F.seq K).stage i).carrier ⊤

The stage identification of the transported succession of K.

Equations

• AnalyticManifold.ExtensionCompatibleFamily.stageEquiv ψ F K i = AnalyticManifold.FiniteSuccession.transportAlongStage (M.restrictTransportDiffeomorph ψ (F.nhd K)) ψ.symm (F.seq K) i

theorem AnalyticManifold.ExtensionCompatibleFamily.center_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) (i : Fin (F.seq K).length) : ((transportBack ψ F).seq K).center i = IdealSheaf.pullbackDiffeomorph (stageEquiv ψ F K i.castSucc) ((F.seq K).center i)

The centres of the transported family are the pull-backs of F's along the stage identifications (center_transportAlong).

theorem AnalyticManifold.ExtensionCompatibleFamily.weakTransformSeq_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((F.seq K).length + 1)) : ((transportBack ψ F).seq K).weakTransformSeq (J.restrict ((transportBack ψ F).nhd K)) i = IdealSheaf.pullbackDiffeomorph (stageEquiv ψ F K i) ((F.seq K).weakTransformSeq ((IdealSheaf.transport ψ J).restrict (F.nhd K)) i)

The weak transforms of J|_{U_K} along the transported succession are the pull-backs of those of the re-modelled J along F's (weakTransformSeq_transportAlong with the restriction of the re-modelled sheaf).

theorem AnalyticManifold.ExtensionCompatibleFamily.boundarySeq_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((F.seq K).length + 1)) : ((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) i = IdealSheaf.pullbackDiffeomorph (stageEquiv ψ F K i) ((F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) i)

The boundaries started with E₀|_{U_K} along the transported succession are the pull-backs of those started with the re-modelled E₀ along F's (boundarySeq_transportAlong).

theorem AnalyticManifold.ExtensionCompatibleFamily.strictTransformSubspaceSeq_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((F.seq K).length + 1)) : ((transportBack ψ F).seq K).strictTransformSubspaceSeq (J.restrict ((transportBack ψ F).nhd K)) i = IdealSheaf.pullbackDiffeomorph (stageEquiv ψ F K i) ((F.seq K).strictTransformSubspaceSeq ((IdealSheaf.transport ψ J).restrict (F.nhd K)) i)

The strict transforms of the closed subspace J|_{U_K} along the transported succession are the pull-backs of those of the re-modelled J along F's (strictTransformSubspaceSeq_transportAlong with the restriction of the re-modelled sheaf).

theorem AnalyticManifold.ExtensionCompatibleFamily.isNonsingular_center_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) (i : Fin (F.seq K).length) : (((transportBack ψ F).seq K).center i).IsNonsingular ↔ ((F.seq K).center i).IsNonsingular

The non-singularity of the centres, per compact (clause (i) of the main theorems): the centres of the transported family are non-singular iff F's are (isNonsingular_pullbackDiffeomorph_iff along the stage identification).

theorem AnalyticManifold.ExtensionCompatibleFamily.hasOnlyNormalCrossingsWith_boundarySeq_center_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin (F.seq K).length) : (((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) i.castSucc).HasOnlyNormalCrossingsWith (((transportBack ψ F).seq K).center i) ↔ ((F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) i.castSucc).HasOnlyNormalCrossingsWith ((F.seq K).center i)

The stalk-local boundary clause per compact, for any boundary E₀ on M — a general tool (the main theorems read the family form below).

theorem AnalyticManifold.ExtensionCompatibleFamily.hasOnlyNormalCrossings_boundarySeq_last_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) : (((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) (Fin.last ((transportBack ψ F).seq K).length)).HasOnlyNormalCrossings ↔ ((F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) (Fin.last (F.seq K).length)).HasOnlyNormalCrossings

The stalk-local last-boundary clause per compact — a general tool.

theorem AnalyticManifold.ExtensionCompatibleFamily.weakTransformSeq_last_seq_transportBack_eq_unit_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) : ((transportBack ψ F).seq K).weakTransformSeq (J.restrict ((transportBack ψ F).nhd K)) (Fin.last ((transportBack ψ F).seq K).length) = ⊤ ↔ (F.seq K).weakTransformSeq ((IdealSheaf.transport ψ J).restrict (F.nhd K)) (Fin.last (F.seq K).length) = ⊤

The last weak transform is the unit ideal, per compact (clause (iv) of Main Theorem II''(N)): the last weak transform of J|_{U_K} along the transported succession is the unit ideal iff that of the re-modelled J is (the pull-back of the unit is the unit, and pull-back along an isomorphism is injective).

theorem AnalyticManifold.ExtensionCompatibleFamily.ord_weakTransformSeq_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin ((F.seq K).length + 1)) (y : (((transportBack ψ F).seq K).stage i).carrier) : Manifold.IdealSheaf.ord (((transportBack ψ F).seq K).weakTransformSeq (J.restrict ((transportBack ψ F).nhd K)) i) y = Manifold.IdealSheaf.ord ((F.seq K).weakTransformSeq ((IdealSheaf.transport ψ J).restrict (F.nhd K)) i) ((FiniteSuccession.transportAlongStage (M.restrictTransportDiffeomorph ψ (F.nhd K)) ψ.symm (F.seq K) i) y)

The order of the weak transforms, per compact (clause (ii) of Main Theorem II''(N)): the order of the weak transform at a point of a stage of the transported succession is its order at the identified point (ord_pullbackDiffeomorph along the stage identification).

theorem AnalyticManifold.ExtensionCompatibleFamily.support_center_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) (i : Fin (F.seq K).length) : Manifold.IdealSheaf.support (((transportBack ψ F).seq K).center i) = ⇑(FiniteSuccession.transportAlongStage (M.restrictTransportDiffeomorph ψ (F.nhd K)) ψ.symm (F.seq K) i.castSucc) ⁻¹' Manifold.IdealSheaf.support ((F.seq K).center i)

The support of a centre of the transported succession is the preimage of the support of F's under the stage identification.

The global clauses

theorem AnalyticManifold.ExtensionCompatibleFamily.comap_map_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(transportBack ψ F).map ⋯ J = IdealSheaf.pullbackDiffeomorph (F.space.transportDiffeomorph ψ.symm).symm (Manifold.IdealSheaf.pullback ⇑F.map ⋯ (IdealSheaf.transport ψ J))

The pull-back of J along the transported map is the pull-back, along the identity of the space, of the pull-back of the re-modelled J along F.map.

theorem AnalyticManifold.ExtensionCompatibleFamily.jacobianIdeal_map_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) : (transportBack ψ F).map.jacobianIdeal = IdealSheaf.pullbackDiffeomorph (F.space.transportDiffeomorph ψ.symm).symm F.map.jacobianIdeal

The Jacobian ideal of the transported map is the pull-back of the Jacobian ideal of F.map along the identity of the space: jacobianIdeal_of_square on the square of F.map with the two identities; no unit germ.

theorem AnalyticManifold.ExtensionCompatibleFamily.isNormalCrossingsDivisor_comap_map_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) : IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑(transportBack ψ F).map ⋯ J) ↔ IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑F.map ⋯ (IdealSheaf.transport ψ J))

The divisor clause of the principalization theorem: J.pullback map map.contMDiff is a normal-crossings divisor iff the re-modelled J's pull-back along F.map is.

theorem AnalyticManifold.ExtensionCompatibleFamily.isNormalCrossingsDivisor_jacobianIdeal_mul_pullback_map_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) : ((transportBack ψ F).map.jacobianIdeal * Manifold.IdealSheaf.pullback ⇑(transportBack ψ F).map ⋯ J).IsNormalCrossingsDivisor ↔ (F.map.jacobianIdeal * Manifold.IdealSheaf.pullback ⇑F.map ⋯ (IdealSheaf.transport ψ J)).IsNormalCrossingsDivisor

The Jacobian clause of the principalization theorem BM97, Theorem 1.10, the sentence after it: the product of the Jacobian ideal of the transported map with J.pullback map map.contMDiff is a normal-crossings divisor iff the product for F.map and the re-modelled J is (jacobianIdeal_map_transportBack, comap_map_transportBack, pullbackDiffeomorph_mul, isNormalCrossingsDivisor_pullbackDiffeomorph_iff).

theorem AnalyticManifold.ExtensionCompatibleFamily.isAnalyticIsoOver_map_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) : (transportBack ψ F).map.IsIsoOver (Manifold.IdealSheaf.support J)ᶜ ↔ F.map.IsIsoOver (Manifold.IdealSheaf.support (IdealSheaf.transport ψ J))ᶜ

The isomorphism off the cosupport: the transported map is an analytic isomorphism off the cosupport of J iff F.map is off the cosupport of the re-modelled J (isAnalyticIsoOver_of_square_iff on the square of F.map with the two identities; preimage_support_transport).

theorem AnalyticManifold.ExtensionCompatibleFamily.isAnalyticIsoOver_compl_sing_map_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) : (transportBack ψ F).map.IsIsoOver (Manifold.IdealSheaf.support J \ J.regularLocus)ᶜ ↔ F.map.IsIsoOver (Manifold.IdealSheaf.support (IdealSheaf.transport ψ J) \ (IdealSheaf.transport ψ J).regularLocus)ᶜ

The isomorphism off the singular locus, Włodarczyk's bimeromorphy of the embedded desingularization: the transported map is an isomorphism off Sing(Y) = Y ∖ Reg(Y) of the subspace Y with ideal sheaf J iff F.map is off that of the re-modelled J (isAnalyticIsoOver_of_square_iff on the square of F.map with the two identities; preimage_support_transport, preimage_regularLocus_transport).

The boundary clauses in the simple-normal-crossings family form

theorem AnalyticManifold.ExtensionCompatibleFamily.exists_isSnc_boundarySeq_hasSncWith_center_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) {n : ℕ} (ψE : E ≃L[𝕜] Fin n → 𝕜) (ψS : E' ≃L[𝕜] Fin n → 𝕜) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin (F.seq K).length) : (∃ (G : Manifold.HypersurfaceFamily (((transportBack ψ F).seq K).stage i.castSucc).carrier) (c : ℕ), Manifold.HypersurfaceFamily.IsSnc ψE G ∧ G.idealSheaf = ((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) i.castSucc ∧ Manifold.HypersurfaceFamily.HasSncWith ψE G (Manifold.IdealSheaf.support (((transportBack ψ F).seq K).center i)) c) ↔ ∃ (G : Manifold.HypersurfaceFamily ((F.seq K).stage i.castSucc).carrier) (c : ℕ), Manifold.HypersurfaceFamily.IsSnc ψS G ∧ G.idealSheaf = (F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) i.castSucc ∧ Manifold.HypersurfaceFamily.HasSncWith ψS G (Manifold.IdealSheaf.support ((F.seq K).center i)) c

The boundary clause per compact in the family form, for fixed chart isomorphisms ψE of the model of M and ψS of the standard model: the stage-i boundary of the transported succession is the reduced ideal sheaf of an snc family having snc with the centre iff F's is — the transports of SncFamily.lean along the stage identification (any two chart isomorphisms), the boundary and the centre being pull-backs.

theorem AnalyticManifold.ExtensionCompatibleFamily.exists_isSnc_boundarySeq_last_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) {n : ℕ} (ψE : E ≃L[𝕜] Fin n → 𝕜) (ψS : E' ≃L[𝕜] Fin n → 𝕜) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) : (∃ (G : Manifold.HypersurfaceFamily ((transportBack ψ F).seq K).last.carrier), Manifold.HypersurfaceFamily.IsSnc ψE G ∧ G.idealSheaf = ((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) (Fin.last ((transportBack ψ F).seq K).length)) ↔ ∃ (G : Manifold.HypersurfaceFamily (F.seq K).last.carrier), Manifold.HypersurfaceFamily.IsSnc ψS G ∧ G.idealSheaf = (F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) (Fin.last (F.seq K).length)

The last-boundary clause per compact in the family form (Main Theorem II''(N) (iv); the principalization theorem has no such clause), for fixed chart isomorphisms: isSnc_comap_diffeomorph_iff and idealSheaf_comap_diffeomorph along the identification of the end results.

theorem AnalyticManifold.ExtensionCompatibleFamily.isSncBoundaryWith_boundarySeq_center_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (i : Fin (F.seq K).length) : (((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) i.castSucc).IsSncBoundaryWith (((transportBack ψ F).seq K).center i) ↔ ((F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) i.castSucc).IsSncBoundaryWith ((F.seq K).center i)

The boundary-with-centre clause per compact in the predicate IsSncBoundaryWith of the main theorems: the boundary and the centre are pull-backs along the stage identification, then isSncBoundaryWith_pullbackDiffeomorph_iff at the model isomorphism ψ⁻¹.

theorem AnalyticManifold.ExtensionCompatibleFamily.isSncBoundary_boundarySeq_last_seq_transportBack_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (E₀ : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) : (((transportBack ψ F).seq K).boundarySeq (E₀.restrict ((transportBack ψ F).nhd K)) (Fin.last ((transportBack ψ F).seq K).length)).IsSncBoundary ↔ ((F.seq K).boundarySeq ((IdealSheaf.transport ψ E₀).restrict (F.nhd K)) (Fin.last (F.seq K).length)).IsSncBoundary

The last-boundary clause per compact in the predicate IsSncBoundary of Main Theorem II''(N): isSncBoundary_pullbackDiffeomorph_iff at ψ⁻¹.

Włodarczyk's embedded desingularization per compact

theorem AnalyticManifold.ExtensionCompatibleFamily.isDesingularizedBy_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) (K : TopologicalSpace.Compacts M.carrier) (h : ((IdealSheaf.transport ψ J).restrict (F.nhd K)).IsDesingularizedBy (F.seq K)) : (J.restrict ((transportBack ψ F).nhd K)).IsDesingularizedBy ((transportBack ψ F).seq K)

The clauses of Włodarczyk's embedded desingularization per compact (IdealSheaf.IsDesingularizedBy, [Wlo09, Theorem 2.0.2 (1)–(3), (6)]) carry over from the successions of F and the re-modelled J to those of the transported family and J: every object of the clauses — centres, exceptional divisors, strict transforms, the pull-back of J — is the pull-back of F's along the stage identification, which commutes with the blow-downs (stageMap_transportAlong, composite_transportAlong), and each predicate pulls back (regularLocus_pullbackDiffeomorph, isSncBoundaryWith_pullbackDiffeomorph_iff, IsSncBoundaryTransversalTo.pullbackDiffeomorph, IsMulBoundaryMonomial.pullbackDiffeomorph, at the model isomorphism ψ⁻¹).

theorem AnalyticManifold.ExtensionCompatibleFamily.center_ne_top_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) (h : ∀ (i : Fin (F.seq K).length), (F.seq K).center i ≠ ⊤) (i : Fin ((transportBack ψ F).seq K).length) : ((transportBack ψ F).seq K).center i ≠ ⊤

No empty centre, along the transport: the centres of the transported succession are the pull-backs of F's along the stage identifications (center_seq_transportBack), and the pull-back along an analytic isomorphism is the unit ideal exactly when the ideal sheaf is (pullbackDiffeomorph_top, pullbackDiffeomorph_injective).

theorem AnalyticManifold.ExtensionCompatibleFamily.boundarySeq_le_center_of_codim_le_one_seq_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (K : TopologicalSpace.Compacts M.carrier) (h : ∀ (i : Fin (F.seq K).length) {n' c : ℕ} (ψ' : E' ≃L[𝕜] Fin n' → 𝕜), c ≤ 1 → Manifold.IsClosedSubmanifold ψ' (Manifold.IdealSheaf.support ((F.seq K).center i)) c → c = 1 ∧ ∀ (x : ↑↧((F.seq K).stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal ((F.seq K).boundarySeq ⊤ i.castSucc) x ≤ Manifold.IdealSheaf.stalkIdeal ((F.seq K).center i) x) (i : Fin ((transportBack ψ F).seq K).length) {n' c : ℕ} (ψ' : E ≃L[𝕜] Fin n' → 𝕜) (hc : c ≤ 1) (hC : Manifold.IsClosedSubmanifold ψ' (Manifold.IdealSheaf.support (((transportBack ψ F).seq K).center i)) c) : c = 1 ∧ ∀ (x : ↑↧(((transportBack ψ F).seq K).stage i.castSucc).carrier), Manifold.IdealSheaf.stalkIdeal (((transportBack ψ F).seq K).boundarySeq ⊤ i.castSucc) x ≤ Manifold.IdealSheaf.stalkIdeal (((transportBack ψ F).seq K).center i) x

The centres of codimension at most one, along the transport: a centre of the transported succession which is a closed submanifold of codimension c ≤ 1 is the pull-back of F's centre along the stage identification (support_center_seq_transportBack), a closed submanifold of the same codimension for the chart read through the model isomorphism (IsClosedSubmanifold.preimage_of_square); the containment of the boundary in the centre's ideal sheaf is the pull-back of F's (boundarySeq_seq_transportBack, center_seq_transportBack).

theorem AnalyticManifold.ExtensionCompatibleFamily.isGloballyDesingularizedBy_transportBack {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : AnalyticManifold 𝕜 E} (ψ : E ≃L[𝕜] E') (F : (M.transport ψ).ExtensionCompatibleFamily) (J : M.IdealSheaf) {E₁ Y₁ : F.space.IdealSheaf} (h : (IdealSheaf.transport ψ J).IsGloballyDesingularizedBy F E₁ Y₁) : J.IsGloballyDesingularizedBy (transportBack ψ F) (IdealSheaf.pullbackDiffeomorph (F.space.transportDiffeomorph ψ.symm).symm E₁) (IdealSheaf.pullbackDiffeomorph (F.space.transportDiffeomorph ψ.symm).symm Y₁)

The global objects of the embedded desingularization along the transport: if E and Ỹ on the space of F are the exceptional divisor and the strict transform of the embedded desingularization of the re-modelled J by F (IsGloballyDesingularizedBy), their pull-backs along the identity of the space are those of J by the transported family: the predicates along the identity (IsSncBoundaryTransversalTo.pullbackDiffeomorph, IsMulBoundaryMonomial.pullbackDiffeomorph), the pull-back of J along the transported map being the pull-back of the pull-back of the re-modelled J (pullbackDiffeomorph_comap on the square of F.map with the two identities), and the identifications over a compact through the stage identification (boundarySeq_seq_transportBack, strictTransformSubspaceSeq_seq_transportBack).