The chain families of an exhaustion

Kollár's globalisation glues the resolutions of the members of a cover along their overlaps [Kol07, Proposition 37, proof], and the exceptional divisor of the result has simple normal crossings with support Π⁻¹(X.singularLocus) [Kol07, Theorem 45(3)]; Włodarczyk glues over an exhaustion by relatively compact opens [Wlo09, §4.3]. Here the resolutions Ũ_n → U_n of the members of an exhaustion are glued along their overlaps (ExhaustionGluing, Resolution.lean), and the exceptional families of the levels glue with them when their members are matched level to level by a LABEL — the stage of the common blow-up sequence each member is the exceptional divisor of. Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverFamilyChain.lean does the gluing from four inputs per level: a simple normal crossings family H n on Ũ_n, label maps e n on the members with non-empty trace on the overlap with the next level, the adjacent identity hpair and the covering hsurj. This module supplies them (BEDanFamStar.exists_chainFamilies).

Per level, exists_gluedMembers_resolutionOn_compat (ResolutionOnMembers.lean) gives H n — the glued family of the level's coproduct traces on resolutionOn, with its three clauses and the PIECE-TRACE clause named here PieceTraceCompat: over every base open inside a piece's domain the members are the piece traces, along every isomorphism over X. Its hypothesis is the labelled compatibility of the level's coproduct traces, labelledCompat_pieceTrace (CoproductGluedFamilyCompat.lean).

Per adjacent pair, the two levels are compared through the DOUBLED datum: the levels' data padded to a common dimension and summed (sumPadData), whose single run carries a common label set into which both levels' label sets embed (exists_orderEmbedding_comap_sumInl/InrResIn_sigmaMembers, CoproductSumData.lean) — read at the levels' reading opens through the padded reading opens (padReadingOpens, PadReadingOpens.lean) and the padding identity (exists_padIdentity_of_padPreimageOpens_eq on padIdentityOn). Extending each level's members by the unit ideal along its label map (Function.extend), the local pair identity exists_isoOver_resolutionOn_pair_of_forall_label (CoproductLevelPair.lean) gives, at every point of the overlap, an isomorphism over X of the parts of the two glued resolutions carrying the extended members label by label; the pointwise criterion for one pair of subspaces (compatClosedSubspaces_pair_of_forall_exists_isoOver_two) with the rigidity rigidOver_resolutionOnToSpace turns it into the adjacent identity for every common label (exists_pairLabels). The bed-free bookkeeping exists_chainLabelMaps_of_extend then reads off the label maps: a member with non-empty trace has a partner at the other level, since the extension by ⊤ would otherwise pull the unit ideal back to its trace (cosupport_top; the transition, an isomorphism, reflects the unit ideal: comap_ne_top_of_isIso).

• GlueOver.compatClosedSubspaces_pair_of_forall_exists_isoOver_two — the pointwise criterion for one pair;
• GlueOver.exists_chainLabelMaps_of_extend — the label maps from common label sets;
• LocalEmbeddingData.PieceTraceCompat — the piece-trace clause, named;
• BEDanFamStar.exists_pairLabels — the common label set of two adjacent levels;
• BEDanFamStar.exists_chainFamilies_of_compat, BEDanFamStar.exists_chainFamilies — the chain families. Used by ResolutionSncGlobal.lean.

Not in the sources beyond the statements cited; bookkeeping.

theorem AnalyticSpace.GlueOver.compatClosedSubspaces_pair_of_forall_exists_isoOver_two {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) (hij : i ≠ j) (Zi : (R i).ClosedSubspace) (Zj : (R j).ClosedSubspace) (h : ∀ y ∈ glueOpens X R π dom i j, ∃ (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : P ≤ dom i ⊓ dom j), KLocallyRingedSpace.Hom.toFun (π i) y ∈ P ∧ KLocallyRingedSpace.RigidOver (π i) P ∧ ∃ (θ : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R j).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ ∧ CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P))) (π j) ∧ QuotientSpace.comap (↑(CategoryTheory.CategoryStruct.comp θ ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)))) Zj = QuotientSpace.comap (↑((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P))) Zi) : QuotientSpace.comap (↑(G.t i j)) (restrictGlue π dom j i Zj) = restrictGlue π dom i j Zi

The pointwise criterion for ONE pair of closed subspaces Zi, Zj of two distinct pieces ((37.2) in [Kol07, Proposition 37, proof]) — the family form compatClosedSubspaces_pair_of_forall_exists_isoOver at the family that is Zi at i, Zj at j and the unit ideal elsewhere (Function.update twice on the constant ⊤).

theorem AnalyticSpace.GlueOver.exists_chainLabelMaps_of_extend {K : Type} [RCLike K] {X : AnalyticSpace K} {R : ULift.{u, 0} ℕ → AnalyticSpace K} {π : (i : ULift.{u, 0} ℕ) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ULift.{u, 0} ℕ → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) {Λ : ℕ → Type u} (H : (n : ℕ) → Λ n → (R { down := n }).ClosedSubspace) (Λ' : ℕ → Type u) (l₁ : (n : ℕ) → Λ n → Λ' n) (l₂ : (n : ℕ) → Λ (n + 1) → Λ' n) (hl₁ : ∀ (n : ℕ), Function.Injective (l₁ n)) (hl₂ : ∀ (n : ℕ), Function.Injective (l₂ n)) (hpr : ∀ (n : ℕ) (l : Λ' n), QuotientSpace.comap (↑(G.t { down := n } { down := n + 1 })) (restrictGlue π dom { down := n + 1 } { down := n } (Function.extend (l₂ n) (H (n + 1)) (fun (x : Λ' n) => ⊤) l)) = restrictGlue π dom { down := n } { down := n + 1 } (Function.extend (l₁ n) (H n) (fun (x : Λ' n) => ⊤) l)) : ∃ (e : (n : ℕ) → { σ : Λ n // chainTraceNonempty π dom H n σ } → Λ (n + 1)), (∀ (n : ℕ) (σ : { σ : Λ n // chainTraceNonempty π dom H n σ }), QuotientSpace.comap (↑(G.t { down := n } { down := n + 1 })) (restrictGlue π dom { down := n + 1 } { down := n } (H (n + 1) (e n σ))) = restrictGlue π dom { down := n } { down := n + 1 } (H n ↑σ)) ∧ ∀ (n : ℕ) (τ : Λ (n + 1)), (restrictGlue π dom { down := n + 1 } { down := n } (H (n + 1) τ)).support.Nonempty → ∃ (σ : { σ : Λ n // chainTraceNonempty π dom H n σ }), e n σ = τ

The label maps from common label sets of the adjacent pairs (Kol07, Proposition 37, proof) — injections l₁ n : Λ n → Λ' n, l₂ n : Λ (n+1) → Λ' n into a common label set with the adjacent identity hpr on the members EXTENDED BY ⊤ (Function.extend) give the label maps e n on the members with non-empty trace, the labelled identity hpair and the covering hsurj. A member σ of level n with non-empty trace has a partner τ with l₂ τ = l₁ σ — else its extension at l₁ σ is ⊤, the identity pulls the unit ideal back to the trace of σ, whose cosupport is then empty (cosupport_top); e n σ is that partner and hpair is the identity at l₁ σ. A member τ of level n+1 with non-empty trace has a partner σ with l₁ σ = l₂ τ — else the transition pulls τ's trace back to ⊤, and the transition, an isomorphism, reflects the unit ideal (comap_ne_top_of_isIso); the partner's trace is non-empty by the same reflection, and it is sent to τ by injectivity of l₂.

@[reducible, inline]

abbrev Hironaka.Manifold.LocalEmbeddingData.PieceTraceCompat {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (h : D.ResolutionGluesOn bed) (H : D.sigmaIndex bed (Nonempty.some h).W ⋯ → (D.resolutionOn bed).ClosedSubspace) : Prop

The piece-trace clause, named — for every piece i, every base open P ⊆ U inside the piece's domain and every isomorphism s over X from the part of resolutionOn over P to the part of the piece's local resolution over P, the pull-back of the piece trace of label σ is the pull-back of the member H σ (the last clause of exists_gluedMembers_resolutionOn_compat).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BEDanFamStar.exists_pairLabels {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} (bed : BEDanFamStar 𝕜) (Ex : bed.ExhaustionGluing X) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (n : ℕ) (H₁ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ → ((Ex.D n).resolutionOn bed).ClosedSubspace) (hH₁ : (Ex.D n).PieceTraceCompat bed hbed ⋯ H₁) (H₂ : (Ex.D (n + 1)).sigmaIndex bed (Nonempty.some ⋯).W ⋯ → ((Ex.D (n + 1)).resolutionOn bed).ClosedSubspace) (hH₂ : (Ex.D (n + 1)).PieceTraceCompat bed hbed ⋯ H₂) : ∃ (Λ : Type u) (l₁ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ → Λ) (l₂ : (Ex.D (n + 1)).sigmaIndex bed (Nonempty.some ⋯).W ⋯ → Λ), Function.Injective l₁ ∧ Function.Injective l₂ ∧ ∀ (l : Λ), AnalyticSpace.QuotientSpace.comap (↑(Ex.glue.t { down := n } { down := n + 1 })) (AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n + 1 } { down := n } (Function.extend l₂ H₂ (fun (x : Λ) => ⊤) l)) = AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n } { down := n + 1 } (Function.extend l₁ H₁ (fun (x : Λ) => ⊤) l)

The common label set of two adjacent levels of the exhaustion and the adjacent identity, label by label, on the levels' members extended by ⊤ ([Kol07, Proposition 37, proof]; [Kol07, 34.4] for the padding). The common label set is that of the doubled datum sumPadData (Ex.D n) (Ex.D (n+1)) over the padded reading opens (padReadingOpens, reading the levels' reading opens back: preimageOpens_padExt_padReadingOpens); the levels embed by the label maps of CoproductSumData.lean composed with the padding identity's label isomorphisms read at the levels' reading opens (exists_padIdentity_of_padPreimageOpens_eq on padIdentityOn); the identity is the pointwise criterion for the pair (compatClosedSubspaces_pair_of_forall_exists_isoOver_two), supplied point by point by exists_isoOver_resolutionOn_pair_of_forall_label with the rigidity rigidOver_resolutionOnToSpace.

theorem Hironaka.Manifold.BEDanFamStar.exists_chainFamilies_of_compat {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} (bed : BEDanFamStar 𝕜) (Ex : bed.ExhaustionGluing X) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (hc : ∀ (n : ℕ), (Nonempty.some ⋯).glue.LabelledCompat ((Ex.D n).pieceTrace bed (Nonempty.some ⋯) hbed) fun (x : (Ex.D n).ι) (σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯) => σ) : ∃ (H : (n : ℕ) → (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ → ((Ex.D n).resolutionOn bed).ClosedSubspace), (∀ (n : ℕ), AnalyticSpace.ClosedSubspace.IsSncFamily (H n)) ∧ (∀ (n : ℕ), LocallyFinite fun (σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯) => Manifold.IdealSheaf.support (H n σ)) ∧ (∀ (n : ℕ), ⋃ (σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯), Manifold.IdealSheaf.support (H n σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((Ex.D n).resolutionOnToSpace bed) ⁻¹' X.singularLocus) ∧ ∃ (e : (n : ℕ) → { σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ // AnalyticSpace.GlueOver.chainTraceNonempty (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) H n σ } → (Ex.D (n + 1)).sigmaIndex bed (Nonempty.some ⋯).W ⋯), (∀ (n : ℕ) (σ : { σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ // AnalyticSpace.GlueOver.chainTraceNonempty (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) H n σ }), AnalyticSpace.QuotientSpace.comap (↑(Ex.glue.t { down := n } { down := n + 1 })) (AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n + 1 } { down := n } (H (n + 1) (e n σ))) = AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n } { down := n + 1 } (H n ↑σ)) ∧ ∀ (n : ℕ) (τ : (Ex.D (n + 1)).sigmaIndex bed (Nonempty.some ⋯).W ⋯), (AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n + 1 } { down := n } (H (n + 1) τ)).support.Nonempty → ∃ (σ : { σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ // AnalyticSpace.GlueOver.chainTraceNonempty (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) H n σ }), e n σ = τ

The chain families of an exhaustion from the labelled compatibility of every level ([Kol07, Proposition 37, proof]; [Kol07, Theorem 45(3)]; [Wlo09, §4.3]) — the input of Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverFamilyChain.lean: on every level the simple normal crossings family of exists_gluedMembers_resolutionOn_compat (locally finite, supported on the preimage of the singular locus), and the label maps e n on the members with non-empty trace with the adjacent identity hpair and the covering hsurj, from the common label sets of the adjacent pairs (exists_pairLabels) through exists_chainLabelMaps_of_extend.

theorem Hironaka.Manifold.BEDanFamStar.exists_chainFamilies {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} (bed : BEDanFamStar 𝕜) (Ex : bed.ExhaustionGluing X) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : ∃ (H : (n : ℕ) → (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ → ((Ex.D n).resolutionOn bed).ClosedSubspace), (∀ (n : ℕ), AnalyticSpace.ClosedSubspace.IsSncFamily (H n)) ∧ (∀ (n : ℕ), LocallyFinite fun (σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯) => Manifold.IdealSheaf.support (H n σ)) ∧ (∀ (n : ℕ), ⋃ (σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯), Manifold.IdealSheaf.support (H n σ) = AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((Ex.D n).resolutionOnToSpace bed) ⁻¹' X.singularLocus) ∧ ∃ (e : (n : ℕ) → { σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ // AnalyticSpace.GlueOver.chainTraceNonempty (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) H n σ } → (Ex.D (n + 1)).sigmaIndex bed (Nonempty.some ⋯).W ⋯), (∀ (n : ℕ) (σ : { σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ // AnalyticSpace.GlueOver.chainTraceNonempty (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) H n σ }), AnalyticSpace.QuotientSpace.comap (↑(Ex.glue.t { down := n } { down := n + 1 })) (AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n + 1 } { down := n } (H (n + 1) (e n σ))) = AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n } { down := n + 1 } (H n ↑σ)) ∧ ∀ (n : ℕ) (τ : (Ex.D (n + 1)).sigmaIndex bed (Nonempty.some ⋯).W ⋯), (AnalyticSpace.GlueOver.restrictGlue (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) { down := n + 1 } { down := n } (H (n + 1) τ)).support.Nonempty → ∃ (σ : { σ : (Ex.D n).sigmaIndex bed (Nonempty.some ⋯).W ⋯ // AnalyticSpace.GlueOver.chainTraceNonempty (fun (n : ULift.{u, 0} ℕ) => (Ex.D n.down).resolutionOnToSpace bed) (fun (n : ULift.{u, 0} ℕ) => Ex.U n.down) H n σ }), e n σ = τ

The chain families of an exhaustion ([Kol07, Proposition 37, proof]; [Kol07, Theorem 45(3)]; [Wlo09, §4.3]) — exists_chainFamilies_of_compat with the labelled compatibility of every level's coproduct traces, labelledCompat_pieceTrace (CoproductGluedFamilyCompat.lean). No reducedness of X is assumed.