Włodarczyk's divisor E and strict transform Ỹ on the glued space

The global objects of [Wlo09, Theorem 2.0.2] on the glued space M̃ of a compatible family C (CompatibleFamily.toExtensionCompatibleFamily): the exceptional divisor gluedExceptionalIdeal, the reduced ideal sheaf of the exceptional family glued along the exhaustion (gluedExceptional), and the strict transform globalStrictTransform I, the saturation of the total transform σ^*(I) by the exceptional divisor (IdealSheaf.saturation, [BM97, Proposition 3.13]). Both pull back along the inclusion of every piece to the per-compact objects, the last exceptional divisor and the last strict transform of the succession over the piece (gluedExceptionalIdeal_pullback_toLimitMap, globalStrictTransform_pullback_toLimitMap, the latter by the saturation identity IsDesingularizedBy.strictTransformSubspaceSeq_last_eq_saturation), and the clauses of the theorem hold for them, each read on a piece through the inclusion: E has simple normal crossings (isSncBoundary_gluedExceptionalIdeal) with support the preimage of the singular locus (support_gluedExceptionalIdeal); Ỹ is smooth (isNonsingular_globalStrictTransform) and has simple normal crossings with E transversally (isSncBoundaryTransversalTo_globalStrictTransform); and σ^*(I) = I_Ỹ · I_Ẽ pointwise (isMulBoundaryMonomial_globalStrictTransform). The per-piece hypotheses are the clauses of the embedded desingularization functor on the pieces, with the last exceptional family named explicitly: its simple normal crossings, its reduced ideal sheaf being the last boundary, the desingularization clauses (IsDesingularizedBy), the transversal chart of (3) and the monomial of (6) with respect to that family.

Not in the sources beyond the statement cited; bookkeeping.

The image of a product of ideals

theorem Ideal.map_finset_prod {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {ι : Type u_3} (s : Finset ι) (I : ι → Ideal R) : map f (∏ i ∈ s, I i) = ∏ i ∈ s, map f (I i)

Ideal.map of a finite product of ideals.

The levels of the exhaustion

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.CompatibleFamily.seqLevel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (m : ℕ) : (M.restrict (Manifold.relCompactOpen (exhaustion M) m)).FiniteSuccession

The succession of C over the m-th member of the exhaustion of M.

Equations

• C.seqLevel m = (C.seqOn (Manifold.relCompactOpen (Hironaka.Manifold.exhaustion M) m) ⋯).toSuccession

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.CompatibleFamily.excLevel {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (m : ℕ) : Manifold.HypersurfaceFamily (C.seqLevel m).last.carrier

The last exceptional family of C over the m-th member of the exhaustion.

Equations

• C.excLevel m = C.exceptionalOn (Manifold.relCompactOpen (Hironaka.Manifold.exhaustion M) m) ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.CompatibleFamily.chain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) : Manifold.OpenEmbeddingChain 𝕜 (Fin n → 𝕜)

The chain of end results along the exhaustion.

Equations

• C.chain = C.endResultChain (Hironaka.Manifold.exhaustion M) ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.CompatibleFamily.glueMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) : AnalyticMap C.chain.limitManifold M

The glued blow-down σ : M̃ → M (the map of toExtensionCompatibleFamily), typed on the limit manifold of the chain.

Equations

• C.glueMap = C.toExtensionCompatibleFamily.map

theorem Hironaka.Manifold.CompatibleFamily.space_toExtensionCompatibleFamily {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) : C.toExtensionCompatibleFamily.space = C.chain.limitManifold

theorem Hironaka.Manifold.CompatibleFamily.toSpace_toExtensionCompatibleFamily {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (K : TopologicalSpace.Compacts M.carrier) : C.toExtensionCompatibleFamily.toSpace K = C.chain.toLimitMap (relCompactOpenIndex (exhaustion M) K)

theorem Hironaka.Manifold.CompatibleFamily.glueMap_toLimit {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (m : ℕ) (x : (C.seqLevel m).last.carrier) : C.glueMap (C.chain.toLimit m x) = (M.inclusion (Manifold.relCompactOpen (exhaustion M) m)) ((C.seqLevel m).composite x)

theorem Hironaka.Manifold.CompatibleFamily.pullback_glueMap_pullback_toLimitMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (J : M.IdealSheaf) (m : ℕ) : Manifold.IdealSheaf.pullback ⇑(C.chain.toLimitMap m) ⋯ (Manifold.IdealSheaf.pullback ⇑C.glueMap ⋯ J) = Manifold.IdealSheaf.pullback ⇑(C.seqLevel m).composite ⋯ (J.restrict (Manifold.relCompactOpen (exhaustion M) m))

The pull-back of J along the glued blow-down, read on a piece, is the pull-back of the restriction of J along the composite of the piece.

The global objects

noncomputable def Hironaka.Manifold.CompatibleFamily.gluedExceptionalIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) : C.chain.limitManifold.IdealSheaf

Włodarczyk's exceptional divisor E on M̃: the reduced ideal sheaf of the exceptional family glued along the exhaustion.

Equations

• C.gluedExceptionalIdeal = (C.gluedExceptional (Hironaka.Manifold.exhaustion M)).idealSheaf

noncomputable def Hironaka.Manifold.CompatibleFamily.globalStrictTransform {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (I : M.IdealSheaf) : C.chain.limitManifold.IdealSheaf

Włodarczyk's strict transform Ỹ on M̃: the saturation of the total transform of I by the exceptional divisor ([BM97, Proposition 3.13]).

Equations

• C.globalStrictTransform I = AnalyticManifold.IdealSheaf.saturation (Manifold.IdealSheaf.pullback ⇑C.glueMap ⋯ I) C.gluedExceptionalIdeal

theorem Hironaka.Manifold.CompatibleFamily.isSncBoundary_gluedExceptionalIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) : C.gluedExceptionalIdeal.IsSncBoundary

E is a simple normal crossings divisor.

theorem Hironaka.Manifold.CompatibleFamily.gluedExceptionalIdeal_pullback_toLimitMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (m : ℕ) : Manifold.IdealSheaf.pullback ⇑(C.chain.toLimitMap m) ⋯ C.gluedExceptionalIdeal = (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length)

E pulls back along the inclusion of a piece to the last exceptional divisor of the piece.

theorem Hironaka.Manifold.CompatibleFamily.globalStrictTransform_pullback_toLimitMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (I : M.IdealSheaf) (hdes : ∀ (m : ℕ), (I.restrict (Manifold.relCompactOpen (exhaustion M) m)).IsDesingularizedBy (C.seqLevel m)) (m : ℕ) : Manifold.IdealSheaf.pullback ⇑(C.chain.toLimitMap m) ⋯ (C.globalStrictTransform I) = (C.seqLevel m).strictTransformSubspaceSeq (I.restrict (Manifold.relCompactOpen (exhaustion M) m)) (Fin.last (C.seqLevel m).length)

Ỹ pulls back along the inclusion of a piece to the last strict transform of the piece: the saturation pulls back to the saturation of the pull-backs, which is the strict transform (IsDesingularizedBy.strictTransformSubspaceSeq_last_eq_saturation).

theorem Hironaka.Manifold.CompatibleFamily.preimage_toLimit_support_globalStrictTransform {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (I : M.IdealSheaf) (hdes : ∀ (m : ℕ), (I.restrict (Manifold.relCompactOpen (exhaustion M) m)).IsDesingularizedBy (C.seqLevel m)) (m : ℕ) : ⇑(C.chain.toLimitMap m) ⁻¹' Manifold.IdealSheaf.support (C.globalStrictTransform I) = Manifold.IdealSheaf.support ((C.seqLevel m).strictTransformSubspaceSeq (I.restrict (Manifold.relCompactOpen (exhaustion M) m)) (Fin.last (C.seqLevel m).length))

The support of Ỹ traces on a piece to the support of the last strict transform.

theorem Hironaka.Manifold.CompatibleFamily.support_gluedExceptionalIdeal {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (I : M.IdealSheaf) (hdes : ∀ (m : ℕ), (I.restrict (Manifold.relCompactOpen (exhaustion M) m)).IsDesingularizedBy (C.seqLevel m)) : Manifold.IdealSheaf.support C.gluedExceptionalIdeal = ⇑C.glueMap ⁻¹' (Manifold.IdealSheaf.support I \ I.regularLocus)

|E| = σ⁻¹(Sing Y): on every piece, the support of the last exceptional divisor is the preimage of the singular locus.

theorem Hironaka.Manifold.CompatibleFamily.isNonsingular_globalStrictTransform {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (I : M.IdealSheaf) (hdes : ∀ (m : ℕ), (I.restrict (Manifold.relCompactOpen (exhaustion M) m)).IsDesingularizedBy (C.seqLevel m)) : (C.globalStrictTransform I).IsNonsingular

Ỹ is smooth: at a point of a piece, the local ring of Ỹ is that of the last strict transform of the piece.

theorem Hironaka.Manifold.CompatibleFamily.isSncBoundaryTransversalTo_globalStrictTransform {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (I : M.IdealSheaf) (hdes : ∀ (m : ℕ), (I.restrict (Manifold.relCompactOpen (exhaustion M) m)).IsDesingularizedBy (C.seqLevel m)) (htr : ∀ (m : ℕ), ∀ a ∈ Manifold.IdealSheaf.support ((C.seqLevel m).strictTransformSubspaceSeq (I.restrict (Manifold.relCompactOpen (exhaustion M) m)) (Fin.last (C.seqLevel m).length)), ∃ (k : ℕ) (φ : OpenPartialHomeomorph (C.seqLevel m).last.carrier (Fin n → 𝕜)) (σ : Fin k ↪ Fin n) (cidx : { j : (C.excLevel m).ι // a ∈ (C.excLevel m).hyp j } → Fin n), Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.IdealSheaf.support ((C.seqLevel m).strictTransformSubspaceSeq (I.restrict (Manifold.relCompactOpen (exhaustion M) m)) (Fin.last (C.seqLevel m).length))) φ σ ∧ Manifold.HypersurfaceFamily.IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m) φ a cidx ∧ ∀ (j : { j : (C.excLevel m).ι // a ∈ (C.excLevel m).hyp j }), cidx j ∉ Set.range ⇑σ) : C.gluedExceptionalIdeal.IsSncBoundaryTransversalTo (C.globalStrictTransform I)

Ỹ has simple normal crossings with E, transversally: the transversal chart of a piece, read on M̃, with the glued members through the point indexed by their descendants in the piece (FamilyChain.isSncChartAt_glue_limitChart).

theorem Hironaka.Manifold.CompatibleFamily.isMulBoundaryMonomial_globalStrictTransform {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (C : CompatibleFamily T) (hsnc : ∀ (m : ℕ), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (C.excLevel m)) (hbd : ∀ (m : ℕ), (C.seqLevel m).boundarySeq ⊤ (Fin.last (C.seqLevel m).length) = (C.excLevel m).idealSheaf) (I : M.IdealSheaf) (hdes : ∀ (m : ℕ), (I.restrict (Manifold.relCompactOpen (exhaustion M) m)).IsDesingularizedBy (C.seqLevel m)) (hmon : ∀ (m : ℕ) (x : (C.seqLevel m).last.carrier), ∃ (s : Finset (C.excLevel m).ι) (α : (C.excLevel m).ι → ℕ), (∀ j ∈ s, x ∈ (C.excLevel m).hyp j) ∧ (Manifold.IdealSheaf.pullback ⇑(C.seqLevel m).composite ⋯ (I.restrict (Manifold.relCompactOpen (exhaustion M) m))).stalkIdeal x = Manifold.IdealSheaf.stalkIdeal ((C.seqLevel m).strictTransformSubspaceSeq (I.restrict (Manifold.relCompactOpen (exhaustion M) m)) (Fin.last (C.seqLevel m).length)) x * ∏ j ∈ s, Manifold.vanishingStalk ((C.excLevel m).hyp j) x ^ α j) : AnalyticManifold.IdealSheaf.IsMulBoundaryMonomial (Manifold.IdealSheaf.pullback ⇑C.glueMap ⋯ I) (C.globalStrictTransform I) C.gluedExceptionalIdeal

σ^*(I_Y) = I_Ỹ · I_Ẽ on M̃, pointwise: the monomial of a piece, read on M̃ through the bijective germ map of the inclusion, the members of the piece replaced by their born ancestors.