The final strict transform of the value of bedanFamOfInput

The four theorems of this module describe the final strict transform of the value of the embedded desingularization functor bedanFamOfInput bmod n over a relatively compact open U of a manifold M modelled on 𝕜ⁿ, for a triple T of the class DomBEDan. Write L for the value on U, 𝓘_r for the final marked transform of (T|_U).I at mark 1 along L (markedTransformSeq … 1 (Fin.last _)) and Ỹ for the final ideal-theoretic strict transform (strictTransformSubspaceSeq … (Fin.last _), whose stalks are the saturations of [BM97, Proposition 3.13] at every stage). Each theorem carries one explicit hypothesis hsat: at every stage the saturation stalks of the strict transform have local generators. The hypothesis always holds (saturationStalk_hasLocalGenerators, Hironaka/Manifold/BlowUp/Transform/SaturationFiniteType.lean).

• bedanFamOfInput_cosupport_markedTransformSeq_eq_of_hsat: the cosupport of 𝓘_r is the cosupport of Ỹ;
• bedanFamOfInput_strictTransform_eq_of_hsat: 𝓘_r = Ỹ as ideal sheaves;
• bedanFamOfInput_isNonsingular_strictTransform_of_hsat: Ỹ is non-singular;
• bedanFamOfInput_exists_adaptedChart_isSncChartAt_of_hsat: at every point of Ỹ there is a chart adapted to Ỹ which is a simple-normal-crossing chart of the exceptional divisors in which no divisor through the point carries a coordinate of Ỹ.

The last two are clause (3) of [Wlo09, Theorem 2.0.2] in its proper form, the shape of the output of Włodarczyk's modified algorithm (the proof of [Wlo09, Theorem 7.4.1]: the final marked transform is the ideal of a smooth submanifold with coordinates transversal to the exceptional divisors). The identification 𝓘_r = Ỹ is what makes that output the strict transform of Y.

Proofs. The cosupport identity is the general assembly cosupport_markedTransformSeq_eq_cosupport_strictTransformSubspaceSeq (Hironaka/Resolution/Analytic/Wlo09/Components.lean) at the value: the order bound ≥ 1 at every stage is bedanFamOfInput_isOfOrderGe, the simple normal crossings of the exceptional families is bedanFamOfInput_isSnc_totalTransformSeq, and the coordinate shape of 𝓘_r at its support points is the field output_isSmoothSubmanifoldIdeal of the underlying BMOmodFam, read through the empty-boundary bridge (isSmoothTransversalIdealAt_totalTransformSeqFrom_iff_of_isEmpty). For 𝓘_r = Ỹ: 𝓘_r ≤ Ỹ is the chain inequality markedTransformSeq_le_strictTransformSubspaceSeq; for Ỹ ≤ 𝓘_r stalkwise, off the support both are the unit ideal, and at a support point 𝓘_r is a coordinate ideal on a chart, the stalk of Ỹ lies in the vanishing ideal of its cosupport (stalkIdeal_le_vanishingStalk_of_subset_cosupport), which is the cosupport of 𝓘_r by the first theorem, and that vanishing ideal is the stalk of 𝓘_r by the local Hadamard lemma (vanishingStalk_cosupport_eq_stalkIdeal_of_eq_span_coord). Non-singularity is the regularity of the quotient by a coordinate ideal (isRegularLocalRing_quotient_span_coord through mem_reg_toAnalyticSpace_iff), and the chart of the coordinate shape is the adapted simple-normal-crossing chart, with the proper conjunct cidx j ≠ σ i.

theorem Hironaka.Manifold.bedanFamOfInput_cosupport_markedTransformSeq_eq_of_hsat (𝕜 : 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)) (hsat : ∀ (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I i.castSucc))) : Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I 1 (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)) = Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length))

The cosupport of the final marked transform 𝓘_r of the value over U is the cosupport of the final strict transform Ỹ, under the hypothesis hsat (always satisfied) that the saturation stalks of the strict transform have local generators at every stage.

theorem Hironaka.Manifold.bedanFamOfInput_strictTransform_eq_of_hsat (𝕜 : 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)) (hsat : ∀ (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I i.castSucc))) : (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I 1 (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length) = (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)

The final marked transform 𝓘_r of the value over U is the final strict transform Ỹ, as ideal sheaves, under hsat: Kollár's marked transform at mark 1 along the sequence produces the strict transform of Y once its output is the ideal of a smooth submanifold.

theorem Hironaka.Manifold.bedanFamOfInput_isNonsingular_strictTransform_of_hsat (𝕜 : 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)) (hsat : ∀ (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I i.castSucc))) : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).toAnalyticSpace.IsNonsingular

The final strict transform of the value over U is non-singular (IsNonsingular of the closed subspace), under hsat: the first conjunct of clause (3) of [Wlo09, Theorem 2.0.2].

theorem Hironaka.Manifold.bedanFamOfInput_exists_adaptedChart_isSncChartAt_of_hsat (𝕜 : 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)) (hsat : ∀ (i : Fin (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I i.castSucc))) (x : ↑↧((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stage (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).carrier) : x ∈ Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)) → ∃ (c : ℕ) (φ : OpenPartialHomeomorph ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.stage (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).carrier (Fin n → 𝕜)) (σ : Fin c ↪ Fin n) (cidx : { j : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).ι // x ∈ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).hyp j } → Fin n), Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.IdealSheaf.support ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.strictTransformSubspaceSeq (T.pullback (M.inclusion U) ⋯).I (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length))) φ σ ∧ Manifold.HypersurfaceFamily.IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)) φ x cidx ∧ ∀ (j : { j : ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).ι // x ∈ ((((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.totalTransformSeq (Fin.last (((bedanFamOfInput 𝕜 bmod n).fam T hT).seqOn U hU).toSuccession.length)).hyp j }), cidx j ∉ Set.range ⇑σ

At every point of the final strict transform of the value over U there is a chart adapted to it which is a simple-normal-crossing chart of the exceptional divisors, no divisor through the point carrying a coordinate of the strict transform (the proper form of clause (3) of [Wlo09, Theorem 2.0.2]), under hsat.