A closed subspace containing connected components of the ambient manifold

Włodarczyk's embedded desingularization [Wlo09, Theorem 2.0.2] places no condition on the closed subspace Y ⊆ M beyond its being a subspace, while the embedded desingularization functor of this library takes a triple whose ideal sheaf has nonzero stalks (AnalyticTriple.isNonzeroEverywhere). By the identity theorem the set Z of points at which the ideal sheaf 𝓘_Y vanishes is open and closed (IdealSheaf.isClopen_setOf_stalkIdeal_eq_bot), a union of connected components of M contained in Y. On it the desingularization is the identity, and the functor is applied to the ideal sheaf which is 𝓘_Y off Z and the unit ideal on Z:

• IdealSheaf.unitOn Z: the ideal sheaf which is the unit ideal on the clopen set Z and zero off it, and IdealSheaf.unitOnZeroStalks I = I + unitOn {x | I_x = 0}, the ideal sheaf I made the unit ideal on the components where it vanishes: reduced when I is, with nonzero stalks, and with the same singular locus Sing(Y) = Y ∖ Reg(Y) as I (a point where I vanishes is a simple point of Y, the local ring of Y there being the regular local ring 𝒪_{M,x}).
• FiniteSuccession.stalkIdeal_strictTransformSubspaceSeq_congr: the strict transforms of two ideal sheaves agree at every point over the set where the ideal sheaves agree — the strict transform under a blow-up is the saturation of the total transform, a stalk-wise construction.
• IdealSheaf.IsDesingularizedBy.of_eq_off_clopen: the clauses of [Wlo09, Theorem 2.0.2] on a succession transfer from I' to I when I = I' off a clopen set Z, I = 0 and I' = 1 on Z, and the centres lie over Sing(Y'): over Z nothing is blown up, the exceptional divisor is empty, and the strict transform of I is the zero ideal, whose closed subspace is the ambient manifold itself, smooth and trivially transversal to the empty divisor.

The unit ideal on a clopen set

theorem AnalyticManifold.IdealSheaf.hasLocalGenerators_unitOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (Z : Set M.carrier) (hZ : IsClopen Z) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↧M.carrier) => if x ∈ Z then ⊤ else ⊥

The stalks of the ideal sheaf which is the unit ideal on the clopen set Z and zero off it have local generators: the section 1 on Z, no section on its complement.

noncomputable def AnalyticManifold.IdealSheaf.unitOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (Z : Set M.carrier) (hZ : IsClopen Z) : M.IdealSheaf

The ideal sheaf which is the unit ideal on the clopen set Z and zero off it.

Equations

• AnalyticManifold.IdealSheaf.unitOn Z hZ = Manifold.IdealSheaf.ofStalks (Manifold.structureSheaf 𝕜 E M.carrier) (fun (x : ↑↧M.carrier) => if x ∈ Z then ⊤ else ⊥) ⋯

theorem AnalyticManifold.IdealSheaf.stalkIdeal_unitOn_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : IsClopen Z) {x : M.carrier} (hx : x ∈ Z) : Manifold.IdealSheaf.stalkIdeal (unitOn Z hZ) x = ⊤

theorem AnalyticManifold.IdealSheaf.stalkIdeal_unitOn_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : IsClopen Z) {x : M.carrier} (hx : x ∉ Z) : Manifold.IdealSheaf.stalkIdeal (unitOn Z hZ) x = ⊥

An ideal sheaf made the unit ideal on the components where it vanishes

@[reducible, inline]

abbrev AnalyticManifold.IdealSheaf.zeroLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) : Set M.carrier

The clopen set of points at which I vanishes (isClopen_setOf_stalkIdeal_eq_bot, the identity theorem): the union of the connected components of M on which I = 0.

Equations

• I.zeroLocus = {x : M.carrier | Manifold.IdealSheaf.stalkIdeal I x = ⊥}

theorem AnalyticManifold.IdealSheaf.isClopen_zeroLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) : IsClopen I.zeroLocus

noncomputable def AnalyticManifold.IdealSheaf.unitOnZeroStalks {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) : M.IdealSheaf

The ideal sheaf I made the unit ideal on the components where it vanishes: I + unitOn {x | I_x = 0}, whose stalk is I_x where I_x ≠ 0 and the unit ideal where I_x = 0.

Equations

• I.unitOnZeroStalks = I + AnalyticManifold.IdealSheaf.unitOn I.zeroLocus ⋯

theorem AnalyticManifold.IdealSheaf.stalkIdeal_unitOnZeroStalks_of_eq_bot {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {x : M.carrier} (hx : Manifold.IdealSheaf.stalkIdeal I x = ⊥) : Manifold.IdealSheaf.stalkIdeal I.unitOnZeroStalks x = ⊤

theorem AnalyticManifold.IdealSheaf.stalkIdeal_unitOnZeroStalks_of_ne_bot {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) {x : M.carrier} (hx : Manifold.IdealSheaf.stalkIdeal I x ≠ ⊥) : Manifold.IdealSheaf.stalkIdeal I.unitOnZeroStalks x = Manifold.IdealSheaf.stalkIdeal I x

theorem AnalyticManifold.IdealSheaf.isReduced_unitOnZeroStalks {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) (hI : I.IsReduced) : I.unitOnZeroStalks.IsReduced

I made the unit ideal on its zero components is reduced when I is.

theorem AnalyticManifold.IdealSheaf.isNonzeroEverywhere_unitOnZeroStalks {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) [FiniteDimensional 𝕜 E] : Manifold.IdealSheaf.IsNonzeroEverywhere I.unitOnZeroStalks

I made the unit ideal on its zero components has nonzero stalks.

theorem AnalyticManifold.IdealSheaf.zeroLocus_subset_regularLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) [FiniteDimensional 𝕜 E] : I.zeroLocus ⊆ I.regularLocus

A point at which I vanishes is a simple point of the subspace of I: the local ring there is 𝒪_{M,x}/0 ≅ 𝒪_{M,x}, a regular local ring.

theorem AnalyticManifold.IdealSheaf.notMem_regularLocus_of_stalkIdeal_eq_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {J : M.IdealSheaf} {x : M.carrier} (hx : Manifold.IdealSheaf.stalkIdeal J x = ⊤) : x ∉ J.regularLocus

A point where an ideal sheaf is the unit ideal is not a simple point of its subspace (it is not a point of the subspace: the local ring there is the zero ring, which is not local).

theorem AnalyticManifold.IdealSheaf.support_diff_regularLocus_unitOnZeroStalks {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) [FiniteDimensional 𝕜 E] : Manifold.IdealSheaf.support I.unitOnZeroStalks \ I.unitOnZeroStalks.regularLocus = Manifold.IdealSheaf.support I \ I.regularLocus

I and I made the unit ideal on its zero components have the same singular locus Sing(Y) = Y ∖ Reg(Y): off the zero components the stalks agree, and on them I is a simple point while the unit ideal is not a point of its subspace.

theorem AnalyticManifold.IdealSheaf.unitOnZeroStalks_pullback_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (I : M.IdealSheaf) [FiniteDimensional 𝕜 E] {N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : unitOnZeroStalks (Manifold.IdealSheaf.pullback ⇑g ⋯ I) = Manifold.IdealSheaf.pullback ⇑g ⋯ I.unitOnZeroStalks

Making the unit ideal on the zero components commutes with the pull-back along a local analytic isomorphism g: the germ maps are bijective, so a stalk of the pull-back vanishes exactly when the stalk at the image point does.

The strict transforms of two ideal sheaves agreeing over a set

theorem AnalyticManifold.FiniteSuccession.stalkIdeal_strictTransformSubspaceSeq_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I I' : M.IdealSheaf} {Z : Set M.carrier} (heq : ∀ x ∉ Z, Manifold.IdealSheaf.stalkIdeal I x = Manifold.IdealSheaf.stalkIdeal I' x) (i : Fin (S.length + 1)) (z : (S.stage i).carrier) : (S.stageMap i) z ∉ Z → Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq I i) z = Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq I' i) z

The strict transforms of two ideal sheaves which agree at every point off Z agree at every point over the complement of Z: the strict transform under a blow-up is the saturation of the total transform by the exceptional ideal, which depends only on the stalk of the ideal sheaf at the image point (strictTransformSubspace_eq_ofStalks, saturationStalk).

theorem AnalyticManifold.FiniteSuccession.stalkIdeal_strictTransformSubspaceSeq_last_eq_bot_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I I' : M.IdealSheaf} {Z : Set M.carrier} (hbot : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I x = ⊥) (htop : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I' x = ⊤) (hc : S.CentersOver (Manifold.IdealSheaf.support I' \ I'.regularLocus)) (z : S.last.carrier) (hz : S.composite z ∈ Z) : Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq I (Fin.last S.length)) z = ⊥

Over a set Z on which I vanishes and I' is the unit ideal, if the centres of S lie over Sing(Y'), no exceptional divisor lies over Z, and the last strict transform of I has zero stalk there (stalkIdeal_strictTransformSubspaceSeq_eq_map_of_notMem_support).

theorem AnalyticManifold.FiniteSuccession.exists_adaptedChart_strictTransformSubspaceSeq_of_eq_off_clopen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I I' : M.IdealSheaf} {Z : Set M.carrier} (hZ : IsClopen Z) (hbot : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I x = ⊥) (htop : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I' x = ⊤) (heq : ∀ x ∉ Z, Manifold.IdealSheaf.stalkIdeal I x = Manifold.IdealSheaf.stalkIdeal I' x) (hc : S.CentersOver (Manifold.IdealSheaf.support I' \ I'.regularLocus)) {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {G : Manifold.HypersurfaceFamily S.last.carrier} (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (hpt : ∀ a ∈ Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq I' (Fin.last S.length)), ∃ (c : ℕ) (φ : OpenPartialHomeomorph S.last.carrier E) (σ : Fin c ↪ Fin n) (cidx : { j : G.ι // a ∈ G.hyp j } → Fin n), Manifold.IsAdaptedChart ψ (Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq I' (Fin.last S.length))) φ σ ∧ Manifold.HypersurfaceFamily.IsSncChartAt ψ G φ a cidx ∧ ∀ (j : { j : G.ι // a ∈ G.hyp j }), cidx j ∉ Set.range ⇑σ) (a : ↑↧(S.stage (Fin.last S.length)).carrier) : a ∈ Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq I (Fin.last S.length)) → ∃ (c : ℕ) (φ : OpenPartialHomeomorph S.last.carrier E) (σ : Fin c ↪ Fin n) (cidx : { j : G.ι // a ∈ G.hyp j } → Fin n), Manifold.IsAdaptedChart ψ (Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq I (Fin.last S.length))) φ σ ∧ Manifold.HypersurfaceFamily.IsSncChartAt ψ G φ a cidx ∧ ∀ (j : { j : G.ι // a ∈ G.hyp j }), cidx j ∉ Set.range ⇑σ

The transversal chart clause transfers to an ideal sheaf vanishing on some connected components, with the same simple normal crossings family G: over the clopen Z the strict transform of I has zero stalk, so any snc chart of G restricted over Z is adapted to it in codimension 0; off Z the strict transforms of I and I' agree (stalkIdeal_strictTransformSubspaceSeq_congr), and the chart for I' restricted over the complement of Z serves.

theorem AnalyticManifold.FiniteSuccession.exists_monomial_strictTransformSubspaceSeq_of_eq_off_clopen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I I' : M.IdealSheaf} {Z : Set M.carrier} (hbot : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I x = ⊥) (htop : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I' x = ⊤) (heq : ∀ x ∉ Z, Manifold.IdealSheaf.stalkIdeal I x = Manifold.IdealSheaf.stalkIdeal I' x) (hc : S.CentersOver (Manifold.IdealSheaf.support I' \ I'.regularLocus)) {G : Manifold.HypersurfaceFamily S.last.carrier} (hpt : ∀ (x : S.last.carrier), ∃ (s : Finset G.ι) (α : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ (Manifold.IdealSheaf.pullback ⇑S.composite ⋯ I').stalkIdeal x = Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq I' (Fin.last S.length)) x * ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ α j) (x : S.last.carrier) : ∃ (s : Finset G.ι) (α : G.ι → ℕ), (∀ j ∈ s, x ∈ G.hyp j) ∧ (Manifold.IdealSheaf.pullback ⇑S.composite ⋯ I).stalkIdeal x = Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq I (Fin.last S.length)) x * ∏ j ∈ s, Manifold.vanishingStalk (G.hyp j) x ^ α j

The monomial clause (6) transfers to an ideal sheaf vanishing on some connected components, with the same simple normal crossings family G: over Z both sides are zero, and off Z the stalks of I and I' and of their strict transforms agree.

The transfer of the desingularization clauses

theorem AnalyticManifold.IdealSheaf.IsDesingularizedBy.of_eq_off_clopen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I I' : M.IdealSheaf} {Z : Set M.carrier} (hZ : IsClopen Z) (hbot : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I x = ⊥) (htop : ∀ x ∈ Z, Manifold.IdealSheaf.stalkIdeal I' x = ⊤) (heq : ∀ x ∉ Z, Manifold.IdealSheaf.stalkIdeal I x = Manifold.IdealSheaf.stalkIdeal I' x) (h : I'.IsDesingularizedBy S) (hc : S.CentersOver (Manifold.IdealSheaf.support I' \ I'.regularLocus)) : I.IsDesingularizedBy S

The clauses of [Wlo09, Theorem 2.0.2] transfer to an ideal sheaf vanishing on some connected components. Let Z be clopen, I = 0 and I' = 1 on Z, I = I' off Z, and let the centres of S lie over Sing(Y'). If S desingularizes I' it desingularizes I: the singular loci agree; over Z no centre, hence no exceptional divisor, lies, so the strict transform of I has zero stalk there (stalkIdeal_strictTransformSubspaceSeq_eq_map_of_notMem_support), the ambient stalk is regular, every chart is adapted to the whole space (codimension 0) and is an snc chart of the empty divisor, and σ^*(I) = I_Ỹ · 1 with both sides zero; off Z the strict transforms of I and I' agree (stalkIdeal_strictTransformSubspaceSeq_congr), and the charts of the clauses for I', restricted to the open set over the complement of Z, serve for I.