The embedded desingularization: the normal-crossings clause, and the value on a smooth subspace

The first clauses of [Wlo09, Theorem 2.0.2] for the embedded desingularization functor bedanFamOfInput bmod n of Hironaka/Resolution/Analytic/Wlo09/Basic.lean, per relatively compact open U, from the fields of the modified marked resolution bmod n:

• clause (1): the value on U is, by the order clause isOfOrderGe of bmod n, a smooth blow-up sequence of order ≥ 1 for the restricted (M, 𝓘, 1, E); on DomBEDan the boundary E has no member, so its reduced ideal sheaf is the unit ideal, and the exceptional divisors form a simple normal crossing family at every stage with which every centre has simple normal crossings (bedanFamOfInput_isSnc_totalTransformSeq, bedanFamOfInput_hasSncWith_center, from isSnc_totalTransformSeq and hasSncWith_totalTransformSeq_center);
• the value on an open on which Y is non-singular is the empty sequence (bedanFamOfInput_eq_nil_of_sing_eq_empty): a first centre would be a nonempty subset of supp(𝓘, 1) = Y ∩ U (noEmptyCenters, center_mem_support), every point of which is stopped at stage 0 by the stop rule stopped_never_blownUp (at a regular point the ideal is a coordinate ideal, and there is no divisor). This is Włodarczyk's stop rule, "if I′ = (u) is the ideal of a smooth hypersurface of maximal contact the algorithm is stopped" (the proof of [Wlo09, Theorem 7.4.1]), applied at once;
• its local form (bedanFamOfInput_center_disjoint_fiber_near_regular): for an open V of the ambient manifold on which Y is non-singular, no centre of the value on U lies over U ∩ V, by the previous item on U ⊓ V and the compatibility of the family under restriction to a smaller open (compat, the extension property of [Wlo09, Definition 3.2.6]): the value on U ⊓ V is the empty sequence, so every centre of the pull-back of the value on U to U ⊓ V is empty, while a centre point over U ∩ V would lift to one.

Also here: the regular points of the closed subspace V(J) are the points where the quotient stalk 𝒪_p/J_p is a regular local ring (mem_reg_toAnalyticSpace_iff), this transports along local analytic isomorphisms and passes to smaller opens, and a list of centres whose empty blow-ups erase to the empty list has only empty centres. The algebraic counterparts of clause (1) are BED_isSnc_totalTransformSeq and BED_hasSncWith_center.

The local form is the input for clause (2) of [Wlo09, Theorem 2.0.2], that no centre lies over a simple point of Y, proved in Hironaka/Resolution/Analytic/Wlo09/Assembly.lean.

theorem Manifold.HypersurfaceFamily.support_eq_empty_of_isEmpty {M : Type u} (F : HypersurfaceFamily M) [IsEmpty F.ι] : F.support = ∅

A hypersurface family without members has empty support.

theorem Manifold.HypersurfaceFamily.idealSheaf_eq_top_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : HypersurfaceFamily M) [IsEmpty F.ι] : F.idealSheaf = ⊤

The reduced ideal sheaf of a hypersurface family without members is the unit ideal sheaf.

theorem Hironaka.Manifold.bedanFamOfInput_isOfOrderGe (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I 1 ⊤

The order clause isOfOrderGe of the modified marked resolution, for the embedded desingularization functor and with the unit boundary: on DomBEDan the restricted divisor has no member.

theorem Hironaka.Manifold.bedanFamOfInput_isSnc_totalTransformSeq (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length + 1)) : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq i)

Clause (1) of [Wlo09, Theorem 2.0.2] per open, first half: the exceptional divisors form a simple normal crossing family at every stage.

theorem Hironaka.Manifold.bedanFamOfInput_hasSncWith_center (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length) : Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq i.castSucc) (Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.center i)) ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.codim i)

Clause (1) of [Wlo09, Theorem 2.0.2] per open, second half: every centre has simple normal crossings with the exceptional divisors of its stage.

theorem Manifold.HypersurfaceFamily.isSmoothTransversalIdealAt_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (ψ : E ≃L[𝕜] Fin n → 𝕜) (F : HypersurfaceFamily M) [IsEmpty F.ι] (J : IdealSheaf (structureSheaf 𝕜 E M)) {x : M} (hreg : IsRegularLocalRing (↑((structureSheaf 𝕜 E M).presheaf.stalk x) ⧸ J.stalkIdeal x)) : IsSmoothTransversalIdealAt ψ F J x

The empty-boundary form of the stop predicate IsSmoothTransversalIdealAt of the modified marked resolution: at a point where 𝒪/J is regular, J is locally the ideal of a smooth submanifold, and with no divisor through the point there is nothing to be transversal to.

theorem Hironaka.Manifold.isRegularLocalRing_quotient_of_sing_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) (h : J.toAnalyticSpace.singularLocus = ∅) {p : A.carrier} (hp : p ∈ Manifold.IdealSheaf.support J) : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) A.carrier).presheaf.stalk p) ⧸ Manifold.IdealSheaf.stalkIdeal J p)

A point of the support of J is a simple point of the closed subspace Sp(A)/J iff 𝒪_p/J_p is regular; when the subspace has no singular point every support point qualifies.

theorem Hironaka.Manifold.bedanFamOfInput_eq_nil_of_sing_eq_empty (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (h : (T.pullback (M.inclusion U) ⋯).I.toAnalyticSpace.singularLocus = ∅) : ((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU = AnalyticManifold.BlowUpSequence.nil (M.restrict U)

Over a relatively compact open on which Y is non-singular, the embedded desingularization is the empty sequence: its first centre would be a nonempty subset of supp(𝓘, 1) = Y ∩ U (noEmptyCenters, center_mem_support), every point of which is stopped at stage 0 by the stop rule stopped_never_blownUp (at a regular point the ideal is a coordinate ideal, and there is no divisor). Włodarczyk's stop rule (the proof of [Wlo09, Theorem 7.4.1]), applied at once.

theorem Hironaka.Manifold.Ideal.map_eq_top_iff_of_bijective {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommRing R] [CommRing S] [FunLike F R S] [RingHomClass F R S] (e : F) (he : Function.Bijective ⇑e) (I : Ideal R) : Ideal.map e I = ⊤ ↔ I = ⊤

An ideal is the unit ideal iff its image under a bijective ring homomorphism is.

theorem Hironaka.Manifold.isRegularLocalRing_quotient_stalkIdeal_comap_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (b : N.carrier) : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E N.carrier).presheaf.stalk b) ⧸ (Manifold.IdealSheaf.pullback ⇑h ⋯ J).stalkIdeal b) ↔ IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk (h b)) ⧸ Manifold.IdealSheaf.stalkIdeal J (h b))

Regularity of the quotient stalk 𝒪_b / (h^*J)_b transports along a local analytic isomorphism h to 𝒪_{h b} / J_{h b} (the stalk isomorphism germAlgEquiv).

theorem Hironaka.Manifold.mem_cosupport_comap_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (b : N.carrier) : b ∈ (Manifold.IdealSheaf.pullback ⇑h ⋯ J).support ↔ h b ∈ Manifold.IdealSheaf.support J

The cosupport of a pulled-back ideal sheaf along a local analytic isomorphism is the preimage of the cosupport.

theorem Hironaka.Manifold.mem_reg_toAnalyticSpace_iff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) (y : ↑↑J.toAnalyticSpace.toPresheafedSpace) : y ∈ J.toAnalyticSpace.regularLocus ↔ IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) A.carrier).presheaf.stalk ↑y) ⧸ Manifold.IdealSheaf.stalkIdeal J ↑y)

A point of the closed subspace Sp(A)/J is regular iff the quotient stalk 𝒪_p / J_p at its image is a regular local ring (through QuotientSpace.stalkEquiv).

theorem Hironaka.Manifold.sing_toAnalyticSpace_eq_empty_iff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) : J.toAnalyticSpace.singularLocus = ∅ ↔ ∀ p ∈ Manifold.IdealSheaf.support J, IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 (Fin n → 𝕜) A.carrier).presheaf.stalk p) ⧸ Manifold.IdealSheaf.stalkIdeal J p)

(Sp(A)/J).singularLocus = ∅ iff every support point has a regular quotient stalk.

theorem Hironaka.Manifold.sing_comap_inclusion_eq_empty_of_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : M.IdealSheaf) {W V : TopologicalSpace.Opens M.carrier} (hWV : W ≤ V) (hV : (AnalyticManifold.IdealSheaf.toAnalyticSpace (Manifold.IdealSheaf.pullback ⇑(M.inclusion V) ⋯ J)).singularLocus = ∅) : (AnalyticManifold.IdealSheaf.toAnalyticSpace (Manifold.IdealSheaf.pullback ⇑(M.inclusion W) ⋯ J)).singularLocus = ∅

Non-singularity of the restricted closed subspace passes to a smaller open: Y ∩ W is non-singular when Y ∩ V is, for W ≤ V.

theorem AnalyticManifold.BlowUpSequence.isEmptyAt_of_eraseEmpty_eq_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : L.eraseEmpty = nil M) (i : Fin L.toSuccession.length) : L.toSuccession.IsEmptyAt i

A list whose empty blow-ups erase to the empty list has only empty centres.

theorem Hironaka.Manifold.bedanFamOfInput_center_disjoint_fiber_near_regular (𝕜 : Type) [RCLike 𝕜] (bmod : (n : ℕ) → BMOmodFam 𝕜 n) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (V : TopologicalSpace.Opens M.carrier) (hV : (T.pullback (M.inclusion V) ⋯).I.toAnalyticSpace.singularLocus = ∅) (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length) (x : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stage i.castSucc).carrier) (hx : x ∈ Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.center i)) : (M.inclusion U) (((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stageMap i.castSucc) x) ∉ ↑V

The local form of the previous theorem: for an open V of the ambient manifold on which Y is non-singular, no centre of the value on U lies over U ∩ V. By bedanFamOfInput_eq_nil_of_sing_eq_empty on U ⊓ V and the compatibility of the family under restriction (compat, the extension property of [Wlo09, Definition 3.2.6]): the value on U ⊓ V is the empty sequence, so every centre of the pull-back of the value on U to U ⊓ V is empty, while a centre point over U ∩ V would lift to one.