The glued family on resolutionOn with its piece-compatibility clause

Kollár's descent of the centres through their agreement on the overlaps, (37.2) in [Kol07, Proposition 37, proof]; the glued family's support is Π⁻¹(X.singularLocus) Kol07, Theorem 45(3) ([Wlo09, §4, (3)⇒(4)]; [Wlo09, §4.3]). Clause (3) of exists_functorial_resolution for one datum D is the existence of a labelled family H of closed subspaces of resolutionOn D bed — simple normal crossings, locally finite, with support Π_U⁻¹(X.singularLocus) (exists_gluedMembers_resolutionOn, CoproductGluedFamily.lean). The assembly of the exhaustion's chain families (ExhaustionChainFamilies.lean) needs more than the existence: it compares the members of two adjacent levels over their overlap through the pieces, so it must know that the member of label σ restricts, on the part of resolutionOn over a base open P inside a piece's domain, to the piece trace of label σ — along the identification of that part with the part of the piece's local resolution over P (exists_isoOver_resolutionOn_localResolution, LocalModel.lean). The clause is stated for EVERY isomorphism over X between the two parts, so that no user has to know which identification was chosen: under the independence of the local resolution (hind) the parts of resolutionOn are rigid over X (rigidOver_resolutionOnToSpace, RigidOverLocalResolution.lean), hence any two such isomorphisms agree (isoOver_unique_of_aut), and the clause reduces to the one chosen identification: the inverse of the gluing's partIso, along which the glued member pulls back to the piece's member (comap_ιGlued_gluedMembersOn).

The construction repeats that of CoproductGluedFamily.lean (gluedMembersOn on the chosen gluing's glued space, read into the definition of the resolution through resolutionOnFullPair_eq_of_glues, restricted to the part over U), because the statements there are existential and hide the members.

• KLocallyRingedSpace.exists_iso_restrictOpen_restrictOpen_comap' — the identification of the part of a restriction with the part of the space (Hironaka/AnalyticSpace/RestrictOverLemmas.lean has the unprimed form), with the identity of the two open immersions into the space as its conclusion (the over-Z form follows);
• KLocallyRingedSpace.isIso_restrictTo_of_isIso — the restriction of an isomorphism to matching opens is an isomorphism (used by CoproductLevelPair.lean).
• LocalEmbeddingData.exists_gluedMembers_resolutionOn_compat — the glued family with its piece-compatibility clause.

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

theorem AnalyticSpace.KLocallyRingedSpace.exists_iso_restrictOpen_restrictOpen_comap' {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (g : A ⟶ Z) (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (h : ∀ a ∈ U, Hom.toFun g a ∈ U') (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hOU : ∀ (a : ↑↑A.toPresheafedSpace), Hom.toFun g a ∈ O → a ∈ U) : ∃ (e : (A.restrictOpen U).restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun (CategoryTheory.CategoryStruct.comp (Hom.restrictTo g U U' h) (Z.ofRestrict U')), continuous_toFun := ⋯ }) O) ⟶ A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun g, continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso e ∧ CategoryTheory.CategoryStruct.comp e (A.ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun g, continuous_toFun := ⋯ }) O)) = CategoryTheory.CategoryStruct.comp ((A.restrictOpen U).ofRestrict ((TopologicalSpace.Opens.comap { toFun := Hom.toFun (CategoryTheory.CategoryStruct.comp (Hom.restrictTo g U U' h) (Z.ofRestrict U')), continuous_toFun := ⋯ }) O)) (A.ofRestrict U)

The part of the restriction g|U : A|U ⟶ Z|U' over an open O with g⁻¹O ⊆ U is the part of A over O, as open subspaces of A: the isomorphism isoOfRangeEq of the two open immersions (A|U)|_{(g|U)⁻¹O} ⟶ A|U ⟶ A and A|g⁻¹O ⟶ A, followed by the second, is the first.

theorem AnalyticSpace.KLocallyRingedSpace.isIso_restrictTo_of_isIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) [CategoryTheory.IsIso g] (U : TopologicalSpace.Opens ↑↑A.toPresheafedSpace) (U' : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (hU : ∀ a ∈ U, Hom.toFun g a ∈ U') (hU' : ∀ b ∈ U', Hom.toFun (CategoryTheory.inv g) b ∈ U) : CategoryTheory.IsIso (Hom.restrictTo g U U' hU)

The restriction of an isomorphism to matching opens is an isomorphism — the inverse is the restriction of the inverse (Hom.restrictTo_comp_ofRestrict, Hom.ext_of_comp_ofRestrict).

theorem Hironaka.Manifold.LocalEmbeddingData.gluedMembers_resolutionOnFullPair_compat_aux {𝕜 : 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 ⋯) => σ) (R : AnalyticSpace 𝕜) (π : R ⟶ X) (hp : ⟨R, π⟩ = D.resolutionOnFullPair bed) : ∃ (H : D.sigmaIndex bed (Nonempty.some h).W ⋯ → R.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 π ⁻¹' X.singularLocus ∧ ∀ (i : D.ι), ∀ P ≤ D.pieceDom i ((Nonempty.some h).W i), ∃ (t : R.restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun π, continuous_toFun := ⋯ }) P) ⟶ ((D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso t ∧ CategoryTheory.CategoryStruct.comp (R.ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun π, continuous_toFun := ⋯ }) P)) π = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t (((D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯), continuous_toFun := ⋯ }) P))) ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯) ∧ ∀ (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯), AnalyticSpace.QuotientSpace.comap (↑t) (AnalyticSpace.QuotientSpace.comap (↑(((D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯), continuous_toFun := ⋯ }) P))) (D.pieceTrace bed (Nonempty.some h) hbed i σ)) = AnalyticSpace.QuotientSpace.comap (↑(R.ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun π, continuous_toFun := ⋯ }) P))) (H σ)

The glued members and the chosen identifications on the full glued space, for any pair equal to resolutionOnFullPair — unfolded to the chosen gluing (resolutionOnFullPair_eq_of_glues): the members are gluedMembersOn, the identification of the part over P ≤ pieceDom i (W i) with the part of the piece is the inverse of the gluing's partIso, along which the glued member of label σ pulls back to the piece trace of label σ (comap_ιGlued_gluedMembersOn, partIso_inv_comp_ofRestrict).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_gluedMembers_resolutionOn_compat {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X 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 ∧ ∀ (i : D.ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), ↑P ⊆ U → P ≤ D.pieceDom i ((Nonempty.some h).W i) → ∀ (s : (D.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P) ⟶ ((D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso s → CategoryTheory.CategoryStruct.comp ((D.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P)) (D.resolutionOnToSpace bed) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (((D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯), continuous_toFun := ⋯ }) P))) ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯) → ∀ (σ : D.sigmaIndex bed (Nonempty.some h).W ⋯), AnalyticSpace.QuotientSpace.comap (↑s) (AnalyticSpace.QuotientSpace.comap (↑(((D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.embedding i).toSpaceMap bed ((Nonempty.some h).W i) ⋯), continuous_toFun := ⋯ }) P))) (D.pieceTrace bed (Nonempty.some h) hbed i σ)) = AnalyticSpace.QuotientSpace.comap (↑((D.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P))) (H σ)

The datum's glued family on resolutionOn D bed WITH its piece-compatibility clause ((37.2) in [Kol07, Proposition 37, proof]; [Kol07, Theorem 45(3)]; [Wlo09, §4.3]), with the independence of the local resolution as hind — the family has simple normal crossings, is locally finite, its support is Π_U⁻¹(X.singularLocus), and over every base open P ⊆ U inside the domain of a piece i, along 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 of label σ (rigidity: all such s are the chosen identification).