The glued exceptional family of a local embedding datum

Kollár descends the centres of the run on the disjoint union of a cover through their agreement on the overlaps, (37.2) in [Kol07, Proposition 37, proof]: over a local embedding datum D the functor runs ONCE on the coproduct triple (CoproductExceptionalFamily.lean); the coproduct's exceptional members (sigmaMembers, indexed by the STAGE SET of the single run) trace on every piece's local resolution along the open immersion resIn i (pieceTrace), the trace of label σ being the piece's exceptional member of that label or the unit ideal (RunFamilyRestrict.lean at the summand inclusion sigmaMk i). Kollár's (37.2) says the transitions of the gluing datum carry the trace of label σ on one piece to the trace of the SAME label on the other — the fixed-run device at the padded coproduct (ExceptionalFamilyGlue.lean, FixedRunDevice.lean, CoproductMixedTransition.lean) with the label reconciliation of the common datum; it is taken here as the HYPOTHESIS hcomp/hc, discharged in CoproductGluedFamilyCompat.lean. Under it the traces are a LABELLED compatible family with the identity labelling on the coproduct's stage set (labelledCompat_pieceTrace_of_compat), and the closed-subspace descent of Hironaka/AnalyticSpace/Glue/OverFamily.lean glues them to the datum's exceptional family on the glued space gluedMembersOn, one member per stage, with the restriction identity along ιGlued i, simple normal crossings (isSncFamily_gluedMembersOn: from the pieces' — the coproduct's family of CoproductExceptionalSnc.lean pulled back along the open immersion resIn i, the general IsSncFamily.comap_openImmersion proved here from IsSncFamily.comap_ofRestrict's stalk argument), local finiteness (the coproduct run is finite) and the support identity ⋃ σ, support = Π⁻¹(X.singularLocus) (iUnion_support_gluedMembersOn: the support identity on every piece, read through the open immersions resIn i and q : Sp(Y_i|W_i) → X — mem_reg_iff_of_isOpenImmersion — and the descended map, the pieces covering the glued space). Through the unfolding lemma resolutionOnFullPair_eq_of_glues the family lives on resolutionOnFull D bed and, restricted over U, on resolutionOn D bed with the map resolutionOnToSpace (exists_gluedMembers_resolutionOn, an existence statement keeping the coproduct's stage set as its index — what the exhaustion-level assembly uses level by level).

Not in the sources beyond Kollár's descent; bookkeeping.

theorem AnalyticSpace.ClosedSubspace.IsSncFamily.comap_openImmersion {K : Type} [RCLike K] {X Y : AnalyticSpace K} {ι : Type u} {H : ι → X.ClosedSubspace} (h : IsSncFamily H) (f : Y.toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace) (hf : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑f) : IsSncFamily fun (j : ι) => QuotientSpace.comap (↑f) (H j)

The inverse image of a simple normal crossings family along an OPEN IMMERSION of analytic spaces has simple normal crossings ([Kol07, Definition 24] is pointwise) — the stalk maps are isomorphisms (IsSncFamily.comap_ofRestrict's argument for an arbitrary open immersion).

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.pieceTrace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : D.sigmaIndex bed Γ.W ⋯ → ((D.embedding i).localResolution bed (Γ.W i) ⋯).ClosedSubspace

The coproduct member of label σ traced on piece i along the open immersion resIn i — the piece's exceptional member of that label, or the unit ideal when the stage is empty on the piece (RunFamilyRestrict.lean at the summand inclusion sigmaMk i).

Equations

• D.pieceTrace bed Γ hbed i σ = AnalyticSpace.QuotientSpace.comap (↑(D.resIn bed Γ.W ⋯ hbed i)) (D.sigmaMembers bed Γ.W ⋯ hbed σ)

theorem Hironaka.Manifold.LocalEmbeddingData.isSncFamily_pieceTrace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : AnalyticSpace.ClosedSubspace.IsSncFamily (D.pieceTrace bed Γ hbed i)

The traces on a piece form a simple normal crossings family — isSncFamily_sigmaMembers along the open immersion resIn i.

theorem Hironaka.Manifold.LocalEmbeddingData.labelledCompat_pieceTrace_of_compat {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hcomp : ∀ (σ : D.sigmaIndex bed Γ.W ⋯), Γ.glue.CompatClosedSubspaces fun (i : D.ι) => D.pieceTrace bed Γ hbed i σ) : Γ.glue.LabelledCompat (D.pieceTrace bed Γ hbed) fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ

Compatibility of the traces label by label (Kollár's (37.2)) IS the labelled compatibility LabelledCompat with the identity labelling on the coproduct's stage set (memberOfLabel_lab).

noncomputable def Hironaka.Manifold.LocalEmbeddingData.gluedMembersOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hc : Γ.glue.LabelledCompat (D.pieceTrace bed Γ hbed) fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ) : D.sigmaIndex bed Γ.W ⋯ → Γ.glue.gluedOver.ClosedSubspace

The glued exceptional family of the datum on the glued space, indexed by the coproduct's stage set — glueFamily (Hironaka/AnalyticSpace/Glue/OverFamily.lean) with the identity labelling, under the compatibility hc ((37.2) in [Kol07, Proposition 37, proof]).

Equations

• D.gluedMembersOn bed Γ hbed hc = Γ.glue.glueFamily (D.pieceTrace bed Γ hbed) (fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ) hc

theorem Hironaka.Manifold.LocalEmbeddingData.comap_ιGlued_gluedMembersOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hc : Γ.glue.LabelledCompat (D.pieceTrace bed Γ hbed) fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ) (i : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) : AnalyticSpace.QuotientSpace.comap (↑(Γ.glue.ιGlued i)) (D.gluedMembersOn bed Γ hbed hc σ) = D.pieceTrace bed Γ hbed i σ

The glued member of label σ pulls back along ιGlued i to the trace of label σ on piece i (comap_ιGlued_glueFamily_lab).

theorem Hironaka.Manifold.LocalEmbeddingData.isSncFamily_gluedMembersOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hc : Γ.glue.LabelledCompat (D.pieceTrace bed Γ hbed) fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ) : AnalyticSpace.ClosedSubspace.IsSncFamily (D.gluedMembersOn bed Γ hbed hc)

The glued family is a simple normal crossings family ([Kol07, Theorem 45(3)]; isSncFamily_glueFamily from the pieces' isSncFamily_pieceTrace).

theorem Hironaka.Manifold.LocalEmbeddingData.locallyFinite_gluedMembersOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hc : Γ.glue.LabelledCompat (D.pieceTrace bed Γ hbed) fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ) : LocallyFinite fun (σ : D.sigmaIndex bed Γ.W ⋯) => Manifold.IdealSheaf.support (D.gluedMembersOn bed Γ hbed hc σ)

The glued family is locally finite (locallyFinite_glueFamily; the coproduct run is finite).

theorem Hironaka.Manifold.LocalEmbeddingData.support_pieceTrace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) : Manifold.IdealSheaf.support (D.pieceTrace bed Γ hbed i σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resIn bed Γ.W ⋯ hbed i) ⁻¹' Manifold.IdealSheaf.support (D.sigmaMembers bed Γ.W ⋯ hbed σ)

The support of a trace is the preimage of the coproduct member's support along resIn i (support_comap).

theorem Hironaka.Manifold.LocalEmbeddingData.iUnion_support_pieceTrace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (i : D.ι) : ⋃ (σ : D.sigmaIndex bed Γ.W ⋯), Manifold.IdealSheaf.support (D.pieceTrace bed Γ hbed i σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (Γ.W i) ⋯) ⁻¹' X.singularLocus

The union of the traces' supports on piece i is the preimage of X.singularLocus under the piece's map to X ([Kol07, Theorem 45(3)]) — iUnion_support_sigmaMembers at the coproduct, read through the open immersions resIn i (localResolutionHomOn_comp_map, isOpenImmersion_homOfPullbackEq_of_injective) and q (exists_openImmersion_toSpaceMap_eq) with mem_reg_iff_of_isOpenImmersion at every point.

theorem Hironaka.Manifold.LocalEmbeddingData.iUnion_support_gluedMembersOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (Γ : D.ResolutionGluing bed) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hc : Γ.glue.LabelledCompat (D.pieceTrace bed Γ hbed) fun (x : D.ι) (σ : D.sigmaIndex bed Γ.W ⋯) => σ) : ⋃ (σ : D.sigmaIndex bed Γ.W ⋯), Manifold.IdealSheaf.support (D.gluedMembersOn bed Γ hbed hc σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun Γ.glue.descMap ⁻¹' X.singularLocus

The support of the datum's glued family is Π⁻¹(X.singularLocus) ([Kol07, Theorem 45(3)]) — iUnion_support_glueFamily, the pieces' supports (iUnion_support_pieceTrace), toFun_descMap_ιGlued, the pieces covering the glued space (exists_ιGlued_eq).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_gluedMembers_resolutionOnFull {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (h : D.ResolutionGluesOn bed) (hc : (Nonempty.some h).glue.LabelledCompat (D.pieceTrace bed (Nonempty.some h) hbed) fun (x : D.ι) (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯) => σ) : ∃ (H : D.sigmaIndex bed (Nonempty.some h).W ⋯ → (D.resolutionOnFull bed).ClosedSubspace), AnalyticSpace.ClosedSubspace.IsSncFamily H ∧ (LocallyFinite fun (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯) => Manifold.IdealSheaf.support (H σ)) ∧ ⋃ (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯), Manifold.IdealSheaf.support (H σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnFullMap bed) ⁻¹' X.singularLocus

The datum's glued family on resolutionOnFull D bed — the CHOSEN gluing datum's glued space (the unfolding lemma resolutionOnFullPair_eq_of_glues) — with its three facts, as an existence statement over the coproduct's stage set.

theorem Hironaka.Manifold.LocalEmbeddingData.exists_gluedMembers_resolutionOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (h : D.ResolutionGluesOn bed) (hc : (Nonempty.some h).glue.LabelledCompat (D.pieceTrace bed (Nonempty.some h) hbed) fun (x : D.ι) (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯) => σ) : ∃ (H : D.sigmaIndex bed (Nonempty.some h).W ⋯ → (D.resolutionOn bed).ClosedSubspace), AnalyticSpace.ClosedSubspace.IsSncFamily H ∧ (LocallyFinite fun (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯) => Manifold.IdealSheaf.support (H σ)) ∧ ⋃ (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯), Manifold.IdealSheaf.support (H σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed) ⁻¹' X.singularLocus

The datum's glued family on resolutionOn D bed (the part over U, IsSncFamily.comap_ofRestrict along the open immersion) with its three facts — clause (3) of exists_functorial_resolution for ONE datum ([Kol07, Theorem 45(3)]; [Wlo09, §4.3]): simple normal crossings, locally finite, support Π_U⁻¹(X.singularLocus) under the map resolutionOnToSpace read into X (resolutionOnToSpace = ofRestrict ≫ resolutionOnFullMap, Hom.restrictTo_comp_ofRestrict).