The compatibility of the piece traces along the gluing

Kollár's agreement of the centres on the overlaps, (37.2) in [Kol07, Proposition 37, proof]. The coproduct member of a label is traced on every piece (pieceTrace), and gluedMembersOn (CoproductGluedFamily.lean) glues the traces into a family on the glued local resolution once they are compatible along the transitions with the identity labelling (LabelledCompat). Compatibility of a pair of pieces is a POINTWISE matter (compatClosedSubspaces_pair_of_forall_exists_isoOver, Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverRigidity.lean): at each point of the gluing open an isomorphism over X of the parts over a neighbourhood carrying the one trace to the other, with the rigidity of the piece map over that neighbourhood (rigidOver_pieceToSpace, the only use of hind).

• exists_isoOver_pieces_of_sum (the conjugation lemma): at a point of the domains of a piece of D₁ and a piece of D₂, the mixed-pair transition of the doubled datum sumPadData D₁ D₂ — an isomorphism over X between the parts over P of the two PADDED pieces' local resolutions carrying the doubled run's member of every label — conjugated by the piece isomorphisms of the padding identities (restricted over P, Hom.restrictTo) is an isomorphism over X between the parts over P of the two UNPADDED pieces' local resolutions carrying, for every label σ of the doubled run, the ⊤-extended trace sumLabelTrace of D₂ on the second piece to that of D₁ on the first (comap_resIn_sumPadData_inl/_inr, the label embeddings' clauses, the padding identity's member clause and squares).
• labelledCompat_pieceTrace: the piece traces are compatible with the identity labelling — at the diagonal pair (D, D) with the padded reading opens padReadingOpens, the padding identities from padIdentityOn read at the reading opens of the gluing (exists_padIdentity_of_padPreimageOpens_eq), the two label embeddings, the conjugation lemma at a point of the gluing open, and the label coherence label_route_eq_of_ne_top (DoubledDatumLabels.lean) to read the doubled run's label lab₁ (o₁.symm l) as the label l on both pieces; a label whose member is the unit ideal has all its traces equal to the unit ideal and needs no coherence.

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

theorem Hironaka.Manifold.LocalEmbeddingData.exists_isoOver_pieces_of_sum {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 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))) (V₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D₁.embedding i).G).carrier) (hV₁ : ∀ (i : D₁.ι), IsCompact (closure ↑(V₁ i))) (V₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D₂.embedding j).G).carrier) (hV₂ : ∀ (j : D₂.ι), IsCompact (closure ↑(V₂ j))) (hpre₁ : D₁.padPreimageOpens (Fin.castAddEmb D₂.n) W₁ = V₁) (hpre₂ : D₂.padPreimageOpens (Fin.natAddEmb D₁.n) W₂ = V₂) (o₁ : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁ ≃o D₁.sigmaIndex bed V₁ hV₁) (ψ₁ : bed.localResolutionOn (D₁.padLeftData D₂.n).sigmaTriple ⋯ ((D₁.padLeftData D₂.n).ambImage W₁) ⋯ ⟶ bed.localResolutionOn D₁.sigmaTriple ⋯ (D₁.ambImage V₁) ⋯) (hmem₁ : ∀ (σp : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁), AnalyticSpace.QuotientSpace.comap (↑ψ₁) (D₁.sigmaMembers bed V₁ hV₁ 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 (V₁ i) ⋯), CategoryTheory.IsIso ψᵢ ∧ CategoryTheory.CategoryStruct.comp ψᵢ ((D₁.embedding i).localResolutionToPiece bed (V₁ 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 V₁ hV₁ hbed i)) (o₂ : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂ ≃o D₂.sigmaIndex bed V₂ hV₂) (ψ₂ : bed.localResolutionOn (D₂.padRightData D₁.n).sigmaTriple ⋯ ((D₂.padRightData D₁.n).ambImage W₂) ⋯ ⟶ bed.localResolutionOn D₂.sigmaTriple ⋯ (D₂.ambImage V₂) ⋯) (hmem₂ : ∀ (σp : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂), AnalyticSpace.QuotientSpace.comap (↑ψ₂) (D₂.sigmaMembers bed V₂ hV₂ 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 (V₂ j) ⋯), CategoryTheory.IsIso ψⱼ ∧ CategoryTheory.CategoryStruct.comp ψⱼ ((D₂.embedding j).localResolutionToPiece bed (V₂ 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 V₂ hV₂ 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 σ) = ⊤) (i : D₁.ι) (j : D₂.ι) (x : ↑↑X.toPresheafedSpace) (hxi : x ∈ D₁.pieceDom i (V₁ i)) (hxj : x ∈ D₂.pieceDom j (V₂ j)) : ∃ (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), x ∈ P ∧ P ≤ D₁.pieceDom i (V₁ i) ⊓ D₂.pieceDom j (V₂ j) ∧ ∃ (θ' : ((D₁.embedding i).localResolution bed (V₁ i) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₁.pieceToSpace bed i (V₁ i) ⋯), continuous_toFun := ⋯ }) P) ⟶ ((D₂.embedding j).localResolution bed (V₂ j) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.pieceToSpace bed j (V₂ j) ⋯), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ' ∧ CategoryTheory.CategoryStruct.comp (((D₁.embedding i).localResolution bed (V₁ i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₁.pieceToSpace bed i (V₁ i) ⋯), continuous_toFun := ⋯ }) P)) (D₁.pieceToSpace bed i (V₁ i) ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ' (((D₂.embedding j).localResolution bed (V₂ j) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.pieceToSpace bed j (V₂ j) ⋯), continuous_toFun := ⋯ }) P))) (D₂.pieceToSpace bed j (V₂ j) ⋯) ∧ ∀ (σ : (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯), AnalyticSpace.QuotientSpace.comap (↑(CategoryTheory.CategoryStruct.comp θ' (((D₂.embedding j).localResolution bed (V₂ j) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₂.pieceToSpace bed j (V₂ j) ⋯), continuous_toFun := ⋯ }) P)))) (D₂.sumLabelTrace bed V₂ hV₂ hbed o₂ lab₂ j σ) = AnalyticSpace.QuotientSpace.comap (↑(((D₁.embedding i).localResolution bed (V₁ i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D₁.pieceToSpace bed i (V₁ i) ⋯), continuous_toFun := ⋯ }) P))) (D₁.sumLabelTrace bed V₁ hV₁ hbed o₁ lab₁ i σ)

The mixed-pair transition of the doubled datum, conjugated by the padding identities of the two pieces ((37.2) in [Kol07, Proposition 37, proof]) — at a point x of the domains of the piece i of D₁ and the piece j of D₂ (read at the reading opens V₁, V₂ carried by the padded ones W₁, W₂: hpre₁, hpre₂), an open P ∋ x inside both domains and an isomorphism over X between the parts over P of the two pieces' local resolutions carrying, for every label σ of the doubled run, the ⊤-extended trace of D₂ on the piece j to that of D₁ on the piece i. The binders are the conjuncts of exists_padIdentity_of_padPreimageOpens_eq for the two padded copies (o, ψ with the member clause hmem, and per piece an isomorphism over the piece with the square resIn⁺ i ≫ ψ = ψᵢ ≫ resIn i) and the two label embeddings with their clauses.

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

The piece traces of the coproduct members are compatible along the gluing with the identity labelling ((37.2) in [Kol07, Proposition 37, proof]) — the hypothesis hc of gluedMembersOn and exists_gluedMembers_resolutionOn (CoproductGluedFamily.lean). hind enters only through the rigidity of the piece maps (rigidOver_pieceToSpace).