The base opens of the padded restricted pieces

Two identities of base opens in X for the transition between a padded piece and a piece of the other embedding (CoproductMixedTransition.lean):

• padding and restriction commute on the base opens: the base open of the padded piece E.padAlong σ over the image (in its ambient) of an open Q of the padded SHRUNK ambient of E|V' is the base open of the padded restricted piece (E|V').padAlong σ over Q — the ambient points correspond through pieceAmbientIncl_padExt (PadRestrict.lean) and ambientPoint_padAlong, and a point of the piece whose ambient point lies in the shrunk ambient's image lies in V' (pieceCoord_ambientPoint_mem_restrictAmbient_iff);
• the shear identifies the base opens: for two embeddings F₁, F₂ of one piece with the shear g : W₁ → W₂ of exists_padded_equivalence_hom_point (LocalResolutionShear.lean; bijective local isomorphism, the ideal identity hI, the morphism identity hmor, the point clause hpt), the base open of F₁ over the image in its ambient of an open Q ⊆ W₁ is the base open of F₂ over the image of g(Q) — hpt one way, ambientPoint_mem_of_shear (the shear's opens see the same points) and the injectivity of g the other.

Together: the padded first piece of sumPadData D₁ D₂ (CoproductSumData.lean) over the shear's shrunken open W₁' and the padded second piece over g(W₁') lie over ONE open P of X — the base open of that transition. Not in the sources; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.domOpens_padAlong_pieceAmbientImageOpens {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {n : ℕ} {V V' : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (hV' : IsOpen V') (hsub : V' ⊆ V) {n' : ℕ} (σ : Fin n ↪ Fin n') (Q : TopologicalSpace.Opens (pieceAmbient 𝕜 ((E.restrictPiece hV' hsub).padAlong σ).G).carrier) : (E.padAlong σ).domOpens (pieceAmbientImageOpens ⋯ Q) = ((E.restrictPiece hV' hsub).padAlong σ).domOpens Q

Padding and restriction commute on the base opens — the base open of the padded piece over the image of an open Q of the padded shrunk ambient is the base open of the padded restricted piece over Q.

theorem Hironaka.Manifold.PieceEmbedding.domOpens_imageOpens_eq_of_shear {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {k : ℕ} {V : Set ↑↑X.toPresheafedSpace} (F₁ F₂ : PieceEmbedding 𝕜 k X V) (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 F₁.G).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 F₂.G).carrier) (g : AnalyticMap ((pieceAmbient 𝕜 F₁.G).restrict W₁) ((pieceAmbient 𝕜 F₂.G).restrict W₂)) (hbij : Function.Bijective ⇑g) (hloc : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) (modelWithCornersSelf 𝕜 (Fin k → 𝕜)) ⊤ ⇑g) (hI : F₁.restrictedIdeal W₁ = Manifold.IdealSheaf.pullback ⇑g ⋯ (F₂.restrictedIdeal W₂)) (hmor : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑g ⋯ hI) (F₂.restrictedIdealHom W₂)) F₂.embInv = CategoryTheory.CategoryStruct.comp (F₁.restrictedIdealHom W₁) F₁.embInv) (hpt : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : F₁.ambientPoint y ∈ W₁), ↑(g ⟨F₁.ambientPoint y, hy⟩) = F₂.ambientPoint y) (Q : TopologicalSpace.Opens ((pieceAmbient 𝕜 F₁.G).restrict W₁).carrier) : F₁.domOpens (AnalyticMap.imageOpens ((pieceAmbient 𝕜 F₁.G).inclusion W₁) ⋯ Q) = F₂.domOpens (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 F₂.G).inclusion W₂) g) ⋯ Q)

The shear identifies the base opens ([Kol07, Lemma 39] read on the shear) — the base open of F₁ over the image of an open Q ⊆ W₁ is the base open of F₂ over the image of g(Q): the point clause hpt one way, the shear's opens seeing the same points (ambientPoint_mem_of_shear) and the injectivity of g the other.