The exceptional family of a local embedding datum's COPRODUCT run

Kollár runs the functor once on the disjoint union of an affine cover Kol07, Proposition 37, proof: over a local embedding datum D the functor is run ONCE on the coproduct triple D.sigmaTriple (SigmaTripleData.lean), the ADMISSIBLE input ⊔ᵢ (Gᵢ, 𝓘_{Yᵢ}, ∅) over the relatively compact open D.ambImage W = ⊔ᵢ Wᵢ — the run bed.seqOn D.sigmaTriple D.domBEDan_sigmaTriple (D.ambImage W) _ behind the ambient blow-up factorization of the resolution (D.glueSeq of AmbientEmb.lean is its transport along ambTheta). Its last-stage boundary family — the total transforms of the exceptional divisors from the EMPTY boundary [Kol07, Definition 25] (totalTransformSeq_zero) — is read member by member as closed subspaces of the coproduct's local resolution Sp(Y_r) = bed.localResolutionOn D.sigmaTriple _ (D.ambImage W) _ (HypersurfaceFamily.toClosedSubspaces, the inverse image comap along toAnalyticSpaceι). The members are indexed by THE STAGE SET of the single run (one member per blow-up, empty members allowed): this index set is the LABEL set of the gluing of the exceptional families — within one datum the pieces already share it, and along the open immersion resIn i of each piece's local resolution (AmbientLift.lean) the piece's exceptional members are the coproduct members of the labels in the range of eraseEmptyIdx, the others restricting to the unit ideal (the general identity of RunFamilyRestrict.lean at the summand inclusion sigmaMk i).

The members' closedness is clause (1) of hbed : bed.IsEmbeddedDesing at the last stage of the coproduct run — hbed is the only hypothesis. The facts about this family — simple normal crossings (ClosedSubspace.IsSncFamily) and support Π_Σ⁻¹(Y_Σ.singularLocus) — are in CoproductExceptionalSnc.lean. Not in the sources beyond Kollár's model; bookkeeping.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BEDanFamStar.runFamily {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) : Manifold.HypersurfaceFamily ((bed.seqOn T hT W hW).toSuccession.stage (Fin.last (bed.seqOn T hT W hW).toSuccession.length)).carrier

The last-stage boundary family of the functor's run on T over W (the empty start) — the total transforms of the exceptional divisors ([Kol07, Definition 25]); its index type is the run's stage set.

Equations

• bed.runFamily T hT W hW = (bed.seqOn T hT W hW).toSuccession.totalTransformSeq (Fin.last (bed.seqOn T hT W hW).toSuccession.length)

theorem Hironaka.Manifold.BEDanFamStar.isClosedSubmanifold_runFamily {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) (j : (bed.runFamily T hT W hW).ι) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((bed.runFamily T hT W hW).hyp j) 1

Every member of the run's last-stage boundary family is a closed codimension-one submanifold (clause (1) of hbed at the last stage).

noncomputable def Hironaka.Manifold.BEDanFamStar.runMembers {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (hbed : IsEmbeddedDesing 𝕜 bed) : (bed.runFamily T hT W hW).ι → (bed.localResolutionOn T hT W hW).ClosedSubspace

The run's exceptional members as closed subspaces of its local resolution ([Kol07, Definition 25]; [Wlo09, Theorem 2.0.2(1), (3)]) — the last-stage boundary member j read as the closed subspace of the last stage cut out by its ideal sheaf (HypersurfaceFamily.toClosedSubspaces, closedness from hbed's clause (1)) and traced on localResolutionOn along the inclusion toAnalyticSpaceι (the inverse image comap). sigmaMembers below (a coproduct) is its instance; hbed is its only hypothesis.

Equations

• bed.runMembers T hT W hW hbed j = ((bed.runFamily T hT W hW).toClosedSubspaces ⋯ j).comap (bed.lastIdealOn T hT W hW).toAnalyticSpaceι

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.sigmaRun {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin D.n → 𝕜)) (D.sigmaAmbient.restrict (D.ambImage W))

The single run of the datum ([Kol07, Proposition 37, proof]) — the functor's value on the coproduct triple D.sigmaTriple over D.ambImage W (glueSeq is its transport along ambTheta).

Equations

• D.sigmaRun bed W hW = bed.seqOn D.sigmaTriple ⋯ (D.ambImage W) ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.sigmaFamily {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : Manifold.HypersurfaceFamily ((D.sigmaRun bed W hW).toSuccession.stage (Fin.last (D.sigmaRun bed W hW).toSuccession.length)).carrier

The last-stage boundary family of the single run ([Kol07, Definition 25]) — the total transforms of the exceptional divisors from the empty boundary.

Equations

• D.sigmaFamily bed W hW = (D.sigmaRun bed W hW).toSuccession.totalTransformSeq (Fin.last (D.sigmaRun bed W hW).toSuccession.length)

@[reducible, inline]

abbrev Hironaka.Manifold.LocalEmbeddingData.sigmaIndex {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) : Type u

The label set of the datum — the stage set of the single run (one index per blow-up of the run).

Equations

• D.sigmaIndex bed W hW = (D.sigmaFamily bed W hW).ι

theorem Hironaka.Manifold.LocalEmbeddingData.isClosedSubmanifold_sigmaFamily {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (j : D.sigmaIndex bed W hW) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin D.n → 𝕜)) ((D.sigmaFamily bed W hW).hyp j) 1

Every member of the last-stage boundary family of the single run is a closed codimension-one submanifold (clause (1) of hbed at the last stage).

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sigmaMembers {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : D.sigmaIndex bed W hW → (bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage W) ⋯).ClosedSubspace

The exceptional members of the datum's single run, as closed subspaces of the coproduct's local resolution Sp(Y_r) ([Kol07, Definition 25]; [Wlo09, Theorem 2.0.2(1), (3)]) — the last-stage boundary member j read as the closed subspace of Sp(P_r) cut out by its ideal sheaf (HypersurfaceFamily.toClosedSubspaces, closedness from hbed's clause (1)) and traced on localResolutionOn along the inclusion toAnalyticSpaceι (the inverse image comap): runMembers at the coproduct triple; hbed is its only hypothesis.

Equations

• D.sigmaMembers bed W hW hbed = bed.runMembers D.sigmaTriple ⋯ (D.ambImage W) ⋯ hbed