The shear's opens see the same points of the piece

Kollár's Lemma 39 [Kol07, Lemma 39] read on the shear of exists_padded_equivalence_hom (PieceLemma39Hom.lean): two embeddings F₁, F₂ of one piece X|V (of one dimension), opens W₁, W₂ of their ambients, a SURJECTIVE analytic map g : W₁ → W₂ carrying the restricted ideal of F₂ to that of F₁ (hI) with the morphism identity hmor — "g induces the identity of the piece over W₁, read through the two embeddings" — see the same points: a point of the piece whose F₂-ambient point lies in W₂ has its F₁-ambient point in W₁. (The converse is the shear's point clause hpt.) The argument: the point of Sp(𝓘₂|W₂) over the F₂-ambient point exists (restrictedIdealHom is homOfPullbackEq along the inclusion, range_toFun_homOfPullbackEq), it is the image under homOfPullbackEq g of a point of Sp(𝓘₁|W₁) (g a surjective local isomorphism), hmor reads that point down to the SAME point of the piece, and ambient_comp_embInv_restrictedIdealHom says its F₁-ambient point is the point's coordinate in W₁.

Used by ShearBaseOpens.lean: the base open of the padded first piece over the shear's shrunken open EQUALS the base open of the padded second piece over its image. Not in the sources; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.ambientPoint_mem_of_shear {𝕜 : Type} [RCLike 𝕜] {k : ℕ} {X : AnalyticSpace 𝕜} {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₂)) (hg : Function.Surjective ⇑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) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : F₂.ambientPoint y ∈ W₂) : F₁.ambientPoint y ∈ W₁

The shear's opens see the same points of the piece ([Kol07, Lemma 39] read on the shear) — for a surjective g : W₁ → W₂ with the ideal identity hI and the morphism identity hmor (the two read-down maps of Sp(𝓘₁|W₁) to the piece agree), a point of the piece whose F₂-ambient point lies in W₂ has its F₁-ambient point in W₁.