The common datum of two adjacent levels and its summand inclusions

The labels of two adjacent levels n, n + 1 of the exhaustion are compared through ONE run — the functor's value on the coproduct of ALL the pieces of both levels, padded to a common dimension n₁ + n₂ (PieceEmbedding.padLeft, padRight: the two embeddings (i₁, 0), (0, i₂) into 𝔸ⁿ¹⁺ⁿ² of [Kol07, Lemma 39]), over the union of the reading opens — Kollár's single run on the disjoint union of a cover [Kol07, Proposition 37, proof]. This module builds that datum and its two summand inclusions:

• padLeftData D m, padRightData D m — the same pieces, every embedding padded (dimension D.n + m, m + D.n); sumData D D' h — the pieces of both data, indexed by D.ι ⊕ D'.ι, over U ∪ U' (the embeddings of D' transported along h : D.n = D'.n); sumPadData D₁ D₂ — THE COMMON DATUM (a cast-free literal, equal field by field to sumData (D₁.padLeftData D₂.n) (D₂.padRightData D₁.n) rfl: sumPadData_eq_sumData), whose single run (sigmaRun) is the common run and whose label set (sigmaIndex) is the common label set;
• sumInlAmbient D D' h : D.sigmaAmbient → (sumData D D' h).sigmaAmbient — the inclusion of the first summand's coproduct ambient, the descent (sigmaDescMap) of the summand inclusions sigmaMk (Sum.inl i); it is an analytic open embedding (isAnalyticOpenEmbedding_sumInlAmbient) along which the first datum's coproduct triple is the pull-back of the sum's (isPullbackOf_sigmaTriple_sum, by IdealSheaf.ext_of_comap_sigmaMk summand by summand); at the common datum the two summand inclusions sumPadInlAmbient D₁ D₂, sumInrAmbient D₁ D₂ likewise;
• the reading opens of the common run from those of the two padded data (sumPadOpens), with the first datum's ambient image carried into the sum's (image_sumInlAmbient_ambImage_subset);
• the label maps — exists_orderEmbedding_comap_sumInlResIn_sigmaMembers and its inr counterpart: the GENERAL restriction identity of RunFamilyRestrict.lean ([Kol07, 34.1]) at the summand inclusion, read on the datum's sigmaMembers: an order embedding of the padded level's label set into the common label set, the common run's member of label lab k pulling back along the open immersion sumInlResIn of the local resolutions to the level's member k, the members off the range to ⊤.

The padding identity — the padded level's labels and members against the level's own (exists_isIso_localResolution_padAlong at the coproduct slice) — is the remaining link of the comparison of the two levels; it is CoproductPadIdentity.lean. hbed is the only hypothesis. Not in the sources beyond Kollár's single run; bookkeeping.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.padLeftData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (m : ℕ) : LocalEmbeddingData 𝕜 X U

The left-padded datum ([Kol07, Lemma 39]) — the same pieces, each embedding padded by m trailing coordinates (PieceEmbedding.padLeft); dimension D.n + m.

Equations

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

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.padRightData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (m : ℕ) : LocalEmbeddingData 𝕜 X U

The right-padded datum — each embedding padded by m leading coordinates (PieceEmbedding.padRight); dimension m + D.n.

Equations

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

@[reducible, inline]

abbrev Hironaka.Manifold.LocalEmbeddingData.sumData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (h : D.n = D'.n) : LocalEmbeddingData 𝕜 X (U ∪ U')

The sum of two data of the same dimension over the union of their opens ([Kol07, Proposition 37, proof]) — the pieces of both, indexed by the sum type, the second datum's embeddings transported along h.

Equations

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

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.sumPadData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : LocalEmbeddingData 𝕜 X (U₁ ∪ U₂)

The common padded datum of two adjacent levels — D₁ padded on the right by D₂.n coordinates and D₂ padded on the left by D₁.n, both of dimension D₁.n + D₂.n, summed; its single run is the common run. Written as a literal (not through sumData … rfl): the two padded dimensions are the same term D₁.n + D₂.n, so no transport of the second summand's embeddings is needed — sumData's h ▸ on the inr summand made every identification of the sum's inr pieces with the padded pieces a whnf timeout at the level of morphisms of local resolutions (the comparison of adjacent levels); sumPadData_eq_sumData records that the literal is sumData … rfl — field by field by rfl, the match auxiliaries by cases.

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.sumPadData_eq_sumData {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : D₁.sumPadData D₂ = (D₁.padLeftData D₂.n).sumData (D₂.padRightData D₁.n) ⋯

The literal IS the generic sum of the two padded data along rfl — every field agrees by rfl (the transport along rfl reduces); the two match auxiliaries on the index are identified summand by summand.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sumInlAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (h : D.n = D'.n) : AnalyticMap D.sigmaAmbient (D.sumData D' h).sigmaAmbient

The inclusion of D's coproduct ambient into the sum's — the descent of the summand inclusions sigmaMk (Sum.inl i).

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.sumInlAmbient_comp_sigmaMk {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (h : D.n = D'.n) (i : D.ι) : ContMDiffMap.comp (D.sumInlAmbient D' h) (Manifold.sigmaMk (fun (i : D.ι) => pieceAmbient 𝕜 (D.embedding i).G) i) = Manifold.sigmaMk (fun (k : (D.sumData D' h).ι) => pieceAmbient 𝕜 ((D.sumData D' h).embedding k).G) (Sum.inl i)

The inclusion after a summand inclusion of D is the summand inclusion of the sum.

theorem Hironaka.Manifold.LocalEmbeddingData.isAnalyticOpenEmbedding_sumInlAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (h : D.n = D'.n) : Manifold.IsAnalyticOpenEmbedding (D.sumInlAmbient D' h)

The inclusion is an analytic open embedding (the argument of isCoprodOfOpenEmbeddings_sigmaDescMap) — a local isomorphism (each summand inclusion is one) and injective (Sigma.mk.inj_iff, the summands' ranges disjoint).

theorem Hironaka.Manifold.LocalEmbeddingData.isPullbackOf_sigmaTriple_sum {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (h : D.n = D'.n) : D.sigmaTriple.IsPullbackOf (D.sumData D' h).sigmaTriple (D.sumInlAmbient D' h)

D's coproduct triple is the pull-back of the sum's along the inclusion (the pull-back of [Kol07, 34.1]) — summand by summand (IdealSheaf.ext_of_comap_sigmaMk, isPullbackOf_ambientTriple_sigmaTriple on both sides); the divisors are empty.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sumPadInlAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : AnalyticMap (D₁.padLeftData D₂.n).sigmaAmbient (D₁.sumPadData D₂).sigmaAmbient

The inclusion of the first padded level's coproduct ambient into the common datum's — the descent of the summand inclusions sigmaMk (Sum.inl i) (sumInlAmbient at the literal sumPadData).

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.sumPadInlAmbient_comp_sigmaMk {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (i : D₁.ι) : ContMDiffMap.comp (D₁.sumPadInlAmbient D₂) (Manifold.sigmaMk (fun (i : (D₁.padLeftData D₂.n).ι) => pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G) i) = Manifold.sigmaMk (fun (k : (D₁.sumPadData D₂).ι) => pieceAmbient 𝕜 ((D₁.sumPadData D₂).embedding k).G) (Sum.inl i)

The inl inclusion after a summand inclusion.

theorem Hironaka.Manifold.LocalEmbeddingData.isAnalyticOpenEmbedding_sumPadInlAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : Manifold.IsAnalyticOpenEmbedding (D₁.sumPadInlAmbient D₂)

The inl inclusion is an analytic open embedding.

theorem Hironaka.Manifold.LocalEmbeddingData.isPullbackOf_sigmaTriple_sumPad_inl {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : (D₁.padLeftData D₂.n).sigmaTriple.IsPullbackOf (D₁.sumPadData D₂).sigmaTriple (D₁.sumPadInlAmbient D₂)

The first padded level's coproduct triple is the pull-back of the common datum's along the inl inclusion.

noncomputable def Hironaka.Manifold.LocalEmbeddingData.sumInrAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : AnalyticMap (D₂.padRightData D₁.n).sigmaAmbient (D₁.sumPadData D₂).sigmaAmbient

The inclusion of the second padded level's coproduct ambient into the common datum's — the descent of the summand inclusions sigmaMk (Sum.inr j).

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.sumInrAmbient_comp_sigmaMk {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (j : D₂.ι) : ContMDiffMap.comp (D₁.sumInrAmbient D₂) (Manifold.sigmaMk (fun (j : (D₂.padRightData D₁.n).ι) => pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G) j) = Manifold.sigmaMk (fun (k : (D₁.sumPadData D₂).ι) => pieceAmbient 𝕜 ((D₁.sumPadData D₂).embedding k).G) (Sum.inr j)

The inr inclusion after a summand inclusion.

theorem Hironaka.Manifold.LocalEmbeddingData.isAnalyticOpenEmbedding_sumInrAmbient {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : Manifold.IsAnalyticOpenEmbedding (D₁.sumInrAmbient D₂)

The inr inclusion is an analytic open embedding.

theorem Hironaka.Manifold.LocalEmbeddingData.isPullbackOf_sigmaTriple_sumPad_inr {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) : (D₂.padRightData D₁.n).sigmaTriple.IsPullbackOf (D₁.sumPadData D₂).sigmaTriple (D₁.sumInrAmbient D₂)

The second padded level's coproduct triple is the pull-back of the common datum's along the inr inclusion.

def Hironaka.Manifold.LocalEmbeddingData.sumPadOpens {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (k : (D₁.sumPadData D₂).ι) : TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.sumPadData D₂).embedding k).G).carrier

The reading opens of the common run from those of the two padded levels.

Equations

• D₁.sumPadOpens D₂ W₁ W₂ (Sum.inl i) = W₁ i
• D₁.sumPadOpens D₂ W₁ W₂ (Sum.inr j) = W₂ j

theorem Hironaka.Manifold.LocalEmbeddingData.isCompact_closure_sumPadOpens {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (k : (D₁.sumPadData D₂).ι) : IsCompact (closure ↑(D₁.sumPadOpens D₂ W₁ W₂ k))

Relatively compact reading opens sum to relatively compact ones.

theorem Hironaka.Manifold.LocalEmbeddingData.image_sumInlAmbient_ambImage_subset {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) : ⇑(D₁.sumPadInlAmbient D₂) '' ↑((D₁.padLeftData D₂.n).ambImage W₁) ⊆ ↑((D₁.sumPadData D₂).ambImage (D₁.sumPadOpens D₂ W₁ W₂))

The first padded level's ambient image lands in the common run's (coe_sigmaCoordImage: the images are unions of summand images).

theorem Hironaka.Manifold.LocalEmbeddingData.image_sumInrAmbient_ambImage_subset {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) : ⇑(D₁.sumInrAmbient D₂) '' ↑((D₂.padRightData D₁.n).ambImage W₂) ⊆ ↑((D₁.sumPadData D₂).ambImage (D₁.sumPadOpens D₂ W₁ W₂))

The second padded level's ambient image lands in the common run's.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.sumInlResIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : bed.localResolutionOn (D₁.padLeftData D₂.n).sigmaTriple ⋯ ((D₁.padLeftData D₂.n).ambImage W₁) ⋯ ⟶ bed.localResolutionOn (D₁.sumPadData D₂).sigmaTriple ⋯ ((D₁.sumPadData D₂).ambImage (D₁.sumPadOpens D₂ W₁ W₂)) ⋯

The open immersion of the first padded level's local resolution into the common run's — localResolutionHomOn (LocalResolutionOn.lean) at the inl inclusion.

Equations

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

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.sumInrResIn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : bed.localResolutionOn (D₂.padRightData D₁.n).sigmaTriple ⋯ ((D₂.padRightData D₁.n).ambImage W₂) ⋯ ⟶ bed.localResolutionOn (D₁.sumPadData D₂).sigmaTriple ⋯ ((D₁.sumPadData D₂).ambImage (D₁.sumPadOpens D₂ W₁ W₂)) ⋯

The open immersion of the second padded level's local resolution into the common run's — localResolutionHomOn at the inr inclusion.

Equations

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

theorem Hironaka.Manifold.LocalEmbeddingData.exists_orderEmbedding_comap_sumInlResIn_sigmaMembers {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : ∃ (lab : (D₁.padLeftData D₂.n).sigmaIndex bed W₁ hW₁ ↪o (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯), (∀ (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) ∧ ∀ σ ∉ 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 σ) = ⊤

The label map of the first padded level into the common label set ([Kol07, 34.1]) — the general restriction identity (BEDanFamStar.exists_orderEmbedding_comap_localResolutionHomOn_runMembers) at the inl inclusion, read on the data's sigmaMembers: the common run's member of label lab k pulls back along sumInlResIn to the level's member k, the members off the range to ⊤.

theorem Hironaka.Manifold.LocalEmbeddingData.exists_orderEmbedding_comap_sumInrResIn_sigmaMembers {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U₁ U₂ : Set ↑↑X.toPresheafedSpace} (D₁ : LocalEmbeddingData 𝕜 X U₁) (D₂ : LocalEmbeddingData 𝕜 X U₂) (W₁ : (i : D₁.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₁.padLeftData D₂.n).embedding i).G).carrier) (W₂ : (j : D₂.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 ((D₂.padRightData D₁.n).embedding j).G).carrier) (bed : BEDanFamStar 𝕜) (hW₁ : ∀ (i : (D₁.padLeftData D₂.n).ι), IsCompact (closure ↑(W₁ i))) (hW₂ : ∀ (j : (D₂.padRightData D₁.n).ι), IsCompact (closure ↑(W₂ j))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : ∃ (lab : (D₂.padRightData D₁.n).sigmaIndex bed W₂ hW₂ ↪o (D₁.sumPadData D₂).sigmaIndex bed (D₁.sumPadOpens D₂ W₁ W₂) ⋯), (∀ (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) ∧ ∀ σ ∉ 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 σ) = ⊤

The label map of the second padded level into the common label set ([Kol07, 34.1]) — the general identity at the inr inclusion.