The two-level comparison at the reading opens of the gluing

The padding identity PadIdentityOn D σ Wp hWp bed hbed (CoproductPadIdentity.lean; Kollár's commutation with closed embeddings [Kol07, 34.4], the padding of [Kol07, Lemma 39]) compares the coproduct local resolution of the padded datum D.padAlongData σ over padded reading opens Wp with that of D over the PREIMAGE reading opens padPreimageOpens σ Wp (the zero extension pulled back). The assembly of the exhaustion's chain families meets the datum's local resolution at the reading opens W of the gluing datum, so it needs the identity read at any W equal to those preimages (PadReadingOpens.lean chooses padded opens with prescribed preimages): exists_padIdentity_of_padPreimageOpens_eq is the identity with W in place of padPreimageOpens σ Wp, by substitution. pieceDom_padAlongData is the bookkeeping that the padded piece's base open over Wp i is the datum's over the preimage open (ambientPoint_padAlong: the padded ambient point is the zero extension of the ambient point).

• LocalEmbeddingData.pieceDom_padAlongData;
• LocalEmbeddingData.exists_padIdentity_of_padPreimageOpens_eq;
• LocalEmbeddingData.exists_isoOver_resolutionOn_padPiece_of_members — the leg at one level: the part of resolutionOn over a base open inside a piece's domain is the part of the PADDED piece's local resolution, over X, members carried along;
• LocalEmbeddingData.exists_isoOver_resolutionOn_pair_of_forall_label — the local pair identity of two adjacent levels: leg₁ ≫ θ|P ≫ leg₂⁻¹ with the mixed-pair transition θ (CoproductMixedTransition.lean), label by label of the common padded run. isIso_restrictTo_of_isIso lives in ResolutionOnMembers.lean.

Used by ExhaustionChainFamilies.lean, DoubledDatumLabels.lean and CoproductGluedFamilyCompat.lean. Not in the sources beyond the statements cited; bookkeeping.

theorem Hironaka.Manifold.LocalEmbeddingData.pieceDom_padAlongData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (i : D.ι) : (D.padAlongData σ).pieceDom i (Wp i) = D.pieceDom i (D.padPreimageOpens σ Wp i)

The padded piece's base open over the padded reading open is the datum's over the preimage reading open — the padded ambient point of y is the zero extension of its ambient point (ambientPoint_padAlong), so it lies in Wp i iff the ambient point lies in the preimage.

theorem Hironaka.Manifold.LocalEmbeddingData.exists_padIdentity_of_padPreimageOpens_eq {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hpad : D.PadIdentityOn σ Wp hWp bed hbed) (hpre : D.padPreimageOpens σ Wp = W) : ∃ (o : (D.padAlongData σ).sigmaIndex bed Wp hWp ≃o D.sigmaIndex bed W hW) (ψ : bed.localResolutionOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯ ⟶ bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage W) ⋯), CategoryTheory.IsIso ψ ∧ (∀ (σp : (D.padAlongData σ).sigmaIndex bed Wp hWp), AnalyticSpace.QuotientSpace.comap (↑ψ) (D.sigmaMembers bed W hW hbed (o σp)) = (D.padAlongData σ).sigmaMembers bed Wp hWp hbed σp) ∧ ∀ (i : (D.padAlongData σ).ι), ∃ (ψᵢ : ((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯ ⟶ (D.embedding i).localResolution bed (W i) ⋯), CategoryTheory.IsIso ψᵢ ∧ CategoryTheory.CategoryStruct.comp ψᵢ ((D.embedding i).localResolutionToPiece bed (W i) ⋯) = ((D.padAlongData σ).embedding i).localResolutionToPiece bed (Wp i) ⋯ ∧ CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) ψ = CategoryTheory.CategoryStruct.comp ψᵢ (D.resIn bed W hW hbed i)

The padding identity read at ANY datum reading opens W equal to the preimages of the padded ones ([Kol07, 34.4]; PadReadingOpens.lean chooses such Wp for a given W): the data of PadIdentityOn with W in place of padPreimageOpens σ Wp — the order isomorphism of the label sets, the isomorphism ψ of the coproduct local resolutions carrying the members label by label, and on every piece an isomorphism over the piece with resIn⁺ i ≫ ψ = ψᵢ ≫ resIn i.

theorem Hironaka.Manifold.LocalEmbeddingData.exists_isoOver_resolutionOn_padPiece_of_members {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) {n' : ℕ} (σ : Fin D.n ↪ Fin n') (Wp : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D.padAlongData σ).embedding i).G).carrier) (hWp : ∀ (i : (D.padAlongData σ).ι), IsCompact (closure ↑(Wp i))) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (h : D.ResolutionGluesOn bed) (o : (D.padAlongData σ).sigmaIndex bed Wp hWp ≃o D.sigmaIndex bed (Nonempty.some h).W ⋯) (ψ : bed.localResolutionOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯ ⟶ bed.localResolutionOn D.sigmaTriple ⋯ (D.ambImage (Nonempty.some h).W) ⋯) (hmem : ∀ (σp : (D.padAlongData σ).sigmaIndex bed Wp hWp), AnalyticSpace.QuotientSpace.comap (↑ψ) (D.sigmaMembers bed (Nonempty.some h).W ⋯ hbed (o σp)) = (D.padAlongData σ).sigmaMembers bed Wp hWp hbed σp) (hpiece : ∀ (i : (D.padAlongData σ).ι), ∃ (ψᵢ : ((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯ ⟶ (D.embedding i).localResolution bed ((Nonempty.some h).W i) ⋯), CategoryTheory.IsIso ψᵢ ∧ CategoryTheory.CategoryStruct.comp ψᵢ ((D.embedding i).localResolutionToPiece bed ((Nonempty.some h).W i) ⋯) = ((D.padAlongData σ).embedding i).localResolutionToPiece bed (Wp i) ⋯ ∧ CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) ψ = CategoryTheory.CategoryStruct.comp ψᵢ (D.resIn bed (Nonempty.some h).W ⋯ hbed i)) {Z : AnalyticSpace 𝕜} (ρ : bed.localResolutionOn (D.padAlongData σ).sigmaTriple ⋯ ((D.padAlongData σ).ambImage Wp) ⋯ ⟶ Z) {Λ : Type u} (Sm : Λ → Z.ClosedSubspace) (lab : (D.padAlongData σ).sigmaIndex bed Wp hWp → Λ) (hlab : ∀ (k : (D.padAlongData σ).sigmaIndex bed Wp hWp), AnalyticSpace.QuotientSpace.comap (↑ρ) (Sm (lab k)) = (D.padAlongData σ).sigmaMembers bed Wp hWp hbed k) (hlab' : ∀ l ∉ Set.range lab, AnalyticSpace.QuotientSpace.comap (↑ρ) (Sm l) = ⊤) (H : D.sigmaIndex bed (Nonempty.some h).W ⋯ → (D.resolutionOn bed).ClosedSubspace) (hH : ∀ (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 σ)) (A : Λ → (D.resolutionOn bed).ClosedSubspace) (hA : ∀ (k : (D.padAlongData σ).sigmaIndex bed Wp hWp), A (lab k) = H (o k)) (hA' : ∀ l ∉ Set.range lab, A l = ⊤) (i : D.ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hPU : ↑P ⊆ U) (hPi : P ≤ D.pieceDom i ((Nonempty.some h).W i)) : ∃ (leg : (D.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P) ⟶ (((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.padAlongData σ).pieceToSpace bed i (Wp i) ⋯), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso leg ∧ 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 leg ((((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.padAlongData σ).pieceToSpace bed i (Wp i) ⋯), continuous_toFun := ⋯ }) P))) ((D.padAlongData σ).pieceToSpace bed i (Wp i) ⋯) ∧ ∀ (l : Λ), AnalyticSpace.QuotientSpace.comap (↑(CategoryTheory.CategoryStruct.comp leg ((((D.padAlongData σ).embedding i).localResolution bed (Wp i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D.padAlongData σ).pieceToSpace bed i (Wp i) ⋯), continuous_toFun := ⋯ }) P)))) (AnalyticSpace.QuotientSpace.comap (↑(CategoryTheory.CategoryStruct.comp ((D.padAlongData σ).resIn bed Wp hWp hbed i) ρ)) (Sm l)) = AnalyticSpace.QuotientSpace.comap (↑((D.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P))) (A l)

The leg of the two-level comparison at one level: over a base open P ⊆ U inside the domain of a piece i, an isomorphism over X from the part of resolutionOn over P to the part of the PADDED piece's local resolution over P, carrying — for every label l of a labelled family Sm on a space Z reached from the padded coproduct by ρ (the clauses hlab, hlab' of a label embedding, RunFamilyRestrict.lean) — the trace of Sm l on the padded piece (along resIn⁺ i ≫ ρ) to the member A l of the glued family (A (lab k) = H (o k), ⊤ off the range): the identification of the part with the part of the piece's local resolution (exists_isoOver_resolutionOn_localResolution) followed by the restriction of the inverse of the padding identity's piece isomorphism, with the members through the padding identity's member clause hmem, its square, and the piece-compatibility clause hH.

theorem Hironaka.Manifold.LocalEmbeddingData.exists_isoOver_resolutionOn_pair_of_forall_label {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (h₁ : D₁.ResolutionGluesOn bed) (h₂ : D₂.ResolutionGluesOn bed) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (o₁ : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁ ≃o D₁.sigmaIndex bed (Nonempty.some h₁).W ⋯) (ψ₁ : bed.localResolutionOn (D₁.padLeftData D₂.n).sigmaTriple ⋯ ((D₁.padLeftData D₂.n).ambImage W₁) ⋯ ⟶ bed.localResolutionOn D₁.sigmaTriple ⋯ (D₁.ambImage (Nonempty.some h₁).W) ⋯) (hmem₁ : ∀ (σp : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁), AnalyticSpace.QuotientSpace.comap (↑ψ₁) (D₁.sigmaMembers bed (Nonempty.some h₁).W ⋯ hbed (o₁ σp)) = (D₁.padLeftData D₂.n).sigmaMembers bed W₁ hW₁ hbed σp) (hpiece₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), ∃ (ψᵢ : ((D₁.padLeftData D₂.n).embedding i).localResolution bed (W₁ i) ⋯ ⟶ (D₁.embedding i).localResolution bed ((Nonempty.some h₁).W i) ⋯), CategoryTheory.IsIso ψᵢ ∧ CategoryTheory.CategoryStruct.comp ψᵢ ((D₁.embedding i).localResolutionToPiece bed ((Nonempty.some h₁).W i) ⋯) = ((D₁.padLeftData D₂.n).embedding i).localResolutionToPiece bed (W₁ i) ⋯ ∧ CategoryTheory.CategoryStruct.comp ((D₁.padLeftData D₂.n).resIn bed W₁ hW₁ hbed i) ψ₁ = CategoryTheory.CategoryStruct.comp ψᵢ (D₁.resIn bed (Nonempty.some h₁).W ⋯ hbed i)) (o₂ : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂ ≃o D₂.sigmaIndex bed (Nonempty.some h₂).W ⋯) (ψ₂ : bed.localResolutionOn (D₂.padRightData D₁.n).sigmaTriple ⋯ ((D₂.padRightData D₁.n).ambImage W₂) ⋯ ⟶ bed.localResolutionOn D₂.sigmaTriple ⋯ (D₂.ambImage (Nonempty.some h₂).W) ⋯) (hmem₂ : ∀ (σp : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂), AnalyticSpace.QuotientSpace.comap (↑ψ₂) (D₂.sigmaMembers bed (Nonempty.some h₂).W ⋯ hbed (o₂ σp)) = (D₂.padRightData D₁.n).sigmaMembers bed W₂ hW₂ hbed σp) (hpiece₂ : ∀ (j : (D₂.padRightData D₁.n).ι), ∃ (ψⱼ : ((D₂.padRightData D₁.n).embedding j).localResolution bed (W₂ j) ⋯ ⟶ (D₂.embedding j).localResolution bed ((Nonempty.some h₂).W j) ⋯), CategoryTheory.IsIso ψⱼ ∧ CategoryTheory.CategoryStruct.comp ψⱼ ((D₂.embedding j).localResolutionToPiece bed ((Nonempty.some h₂).W j) ⋯) = ((D₂.padRightData D₁.n).embedding j).localResolutionToPiece bed (W₂ j) ⋯ ∧ CategoryTheory.CategoryStruct.comp ((D₂.padRightData D₁.n).resIn bed W₂ hW₂ hbed j) ψ₂ = CategoryTheory.CategoryStruct.comp ψⱼ (D₂.resIn bed (Nonempty.some h₂).W ⋯ hbed j)) (lab₁ : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁ ↪o (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯) (hlab₁ : ∀ (k : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁), AnalyticSpace.QuotientSpace.comap (↑(D₁.sumInlResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)) ((D₁.sumPadData D₂).sigmaMembers bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed (lab₁ k)) = (D₁.padLeftData D₂.n).sigmaMembers bed W₁ hW₁ hbed k) (hlab₁' : ∀ σ ∉ Set.range ⇑lab₁, AnalyticSpace.QuotientSpace.comap (↑(D₁.sumInlResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)) ((D₁.sumPadData D₂).sigmaMembers bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed σ) = ⊤) (lab₂ : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂ ↪o (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯) (hlab₂ : ∀ (k : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂), AnalyticSpace.QuotientSpace.comap (↑(D₁.sumInrResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)) ((D₁.sumPadData D₂).sigmaMembers bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed (lab₂ k)) = (D₂.padRightData D₁.n).sigmaMembers bed W₂ hW₂ hbed k) (hlab₂' : ∀ σ ∉ Set.range ⇑lab₂, AnalyticSpace.QuotientSpace.comap (↑(D₁.sumInrResIn D₂ W₁ W₂ bed hW₁ hW₂ hbed)) ((D₁.sumPadData D₂).sigmaMembers bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ hbed σ) = ⊤) (hpre₁ : D₁.padPreimageOpens (Fin.castAddEmb D₂.n) W₁ = (Nonempty.some h₁).W) (hpre₂ : D₂.padPreimageOpens (Fin.natAddEmb D₁.n) W₂ = (Nonempty.some h₂).W) (H₁ : D₁.sigmaIndex bed (Nonempty.some h₁).W ⋯ → (D₁.resolutionOn bed).ClosedSubspace) (hH₁ : ∀ (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₁ σ)) (H₂ : D₂.sigmaIndex bed (Nonempty.some h₂).W ⋯ → (D₂.resolutionOn bed).ClosedSubspace) (hH₂ : ∀ (j : D₂.ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), ↑P ⊆ U₂ → P ≤ D₂.pieceDom j ((Nonempty.some h₂).W j) → ∀ (s : (D₂.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P) ⟶ ((D₂.embedding j).localResolution bed ((Nonempty.some h₂).W j) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D₂.embedding j).toSpaceMap bed ((Nonempty.some h₂).W j) ⋯), 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 j).localResolution bed ((Nonempty.some h₂).W j) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D₂.embedding j).toSpaceMap bed ((Nonempty.some h₂).W j) ⋯), continuous_toFun := ⋯ }) P))) ((D₂.embedding j).toSpaceMap bed ((Nonempty.some h₂).W j) ⋯) → ∀ (σ : D₂.sigmaIndex bed (Nonempty.some h₂).W ⋯), AnalyticSpace.QuotientSpace.comap (↑s) (AnalyticSpace.QuotientSpace.comap (↑(((D₂.embedding j).localResolution bed ((Nonempty.some h₂).W j) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((D₂.embedding j).toSpaceMap bed ((Nonempty.some h₂).W j) ⋯), continuous_toFun := ⋯ }) P))) (D₂.pieceTrace bed (Nonempty.some h₂) hbed j σ)) = AnalyticSpace.QuotientSpace.comap (↑((D₂.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P))) (H₂ σ)) (A₁ : (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ → (D₁.resolutionOn bed).ClosedSubspace) (hA₁ : ∀ (k : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁), A₁ (lab₁ k) = H₁ (o₁ k)) (hA₁' : ∀ σ ∉ Set.range ⇑lab₁, A₁ σ = ⊤) (A₂ : (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯ → (D₂.resolutionOn bed).ClosedSubspace) (hA₂ : ∀ (k : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂), A₂ (lab₂ k) = H₂ (o₂ k)) (hA₂' : ∀ σ ∉ Set.range ⇑lab₂, A₂ σ = ⊤) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : ↑O ⊆ U₁ ∩ U₂) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ O) : ∃ (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : P ≤ O), x ∈ P ∧ ∃ (θ : (D₁.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₁.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P) ⟶ (D₂.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ ∧ 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 θ ((D₂.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P))) (D₂.resolutionOnToSpace bed) ∧ ∀ (σ : (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯), AnalyticSpace.QuotientSpace.comap (↑(CategoryTheory.CategoryStruct.comp θ ((D₂.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P)))) (A₂ σ) = AnalyticSpace.QuotientSpace.comap (↑((D₁.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₁.resolutionOnToSpace bed), continuous_toFun := ⋯ }) P))) (A₁ σ)

The local pair identity — the per-point supply for the exhaustion's transitions (compatClosedSubspaces_pair_of_forall_exists_isoOver): at a point x of the overlap of the two levels, an open P ∋ x inside a prescribed open O ⊆ U₁ ∩ U₂ and an isomorphism θ over X between the parts of the two glued resolutions over P carrying, for EVERY common label, the second level's member to the first's — the chain resolutionOn₁|P ≅ Y₁ᵢ|P ≅ Y₁ᵢ⁺|P ≅ Y₂ⱼ⁺|P ≅ Y₂ⱼ|P ≅ resolutionOn₂|P (the piece-compatibility clause, the padding identity's piece isomorphism, the mixed-pair transition, and back) with the members traced through the padding identity's member clause, comap_resIn_sumPadData_inl/_inr (LocalResolutionHomOnComp.lean) and the label embeddings (the ⊤ off-range clauses giving the empty cases), and the transition's member clause; the two levels' padded reading opens read the levels' reading opens (hpre₁, hpre₂).