The shear's isomorphism of padded local resolutions and the local independence of the embedding

Kollár's proof of Theorem 36 compares the local resolutions of one piece Y ⊆ X|V for two embeddings i₁ : Y → G₁ ⊆ 𝕜ⁿ, i₂ : Y → G₂ ⊆ 𝕜ᵐ [Kol07, Theorem 36, proof] (Włodarczyk: the canonical desingularization is independent of the choice of the ambient manifold, [Wlo09, §4, (3)⇒(4)]) in three legs: pad both to dimension n + m (the padded resolution is the resolution of the slice preimage — leg (α), LocalResolutionPad.lean), read the two paddings against each other through Lemma 39's shear g : W₁ → W₂ of the padded ambients (leg (β), this file), and restrict to a smaller open where needed (leg (γ), LocalResolutionRestrict.lean).

Leg (β): the shear

• exists_padded_equivalence_hom_point: Lemma 39 at the morphism level with its point clause — the shear g on opens W₁ ∋ s₁(i₁ x), W₂ of the padded ambients, bijective and a local analytic isomorphism, pulling the right-padded ideal back to the left-padded one, with the identification of the closed subspaces over g equal to the identity of the piece, and carrying s₁(i₁ y) to s₂(i₂ y).
• BEDanFamStar.exists_diffeomorph_last_of_commutes_injective: the commutation of IsEmbeddedDesing with local analytic isomorphisms ([Kol07, 34.1]) along an INJECTIVE local analytic isomorphism g : N → M, at a relatively compact open U' of N: the last stages of the values on U' and on g(U') are diffeomorphic over g and the final strict transforms correspond — the same-model content of the dimension cast (DimensionCast.lean) without the cast.
• PieceEmbedding.localResolutionToPiece_comp_homOfPullbackEq_of_shear: the compatibility Π₂ ∘ m₂ = Π₁ ∘ m₁ for any two last-stage diffeomorphisms over ι₁ and ι₂ ∘ g carrying the final strict transforms — the body of the core, factored out.
• PieceEmbedding.exists_isIso_localResolution_of_shear_core: for a relatively compact open U' of the shear's source W₁, the commutation along the two injective local isomorphisms ι₁ : W₁ ↪ A₁ and ι₂ ∘ g : W₁ → A₂ at the SAME U' gives two last-stage diffeomorphisms from the value on W₁|U', the induced morphisms of closed subspaces are isomorphisms m₁ : Ỹ' ≅ Ỹ₁, m₂ : Ỹ' ≅ Ỹ₂ of the final strict transforms, ψ := m₂ ∘ m₁⁻¹; the compatibility over the piece reduces to Π₂ ∘ m₂ = Π₁ ∘ m₁, read after the isomorphism E₁.emb through the morphism identity of the shear on W₁, the quotient-map squares and the two squares of composites.
• exists_isIso_localResolution_of_shear and its strengthening exists_isIso_localResolution_of_shear' (with the point clause on the right): shrink U' around s₁(i₁ x) inside ι₁⁻¹ V₁ ∩ (ι₂ ∘ g)⁻¹ V₂ (the shrinking lemma exists_opens_isCompact_closure_mem_le), then the core.

The assembly of the three legs

localResolution_independent_local: for x over W₁ and over W₂, the shear's isomorphism at V₁ := p₁⁻¹ W₁, V₂ := p₂⁻¹ W₂ gives U₁, U₂; the shrunken opens W₁' := s₁⁻¹ U₁ ≤ W₁, W₂' := s₂⁻¹ U₂ ≤ W₂ of the unpadded ambients and the open N := (E₁ over W₁') ∩ (E₂ over W₂') ∋ x of the piece; the chain (γ)₁ · (α₁)⁻¹ · (β) · (α₂) · (γ)₂⁻¹ in the relation "isomorphic over N", composed by exists_restrictSet_isIso_trans/_symm, with exists_restrictSet_isIso_of_comp_eq turning each isomorphism over the piece into the relation over N. The global form is localResolution_independent_of_local (LocalResolutionIndependent.lean).

The two small general tools IdealSheaf.isReduced_pullback_of_isLocalDiffeomorph (Hironaka/Manifold/IdealSheaf/ReducedPullback.lean) and PieceEmbedding.domBEDan_ambientTriple_pullback_inclusion put the restricted triple (G, 𝓘_Y, ∅)|_W in the class DomBEDan.

theorem Hironaka.Manifold.exists_opens_isCompact_closure_mem_le {M : Type u_1} [TopologicalSpace M] [LocallyCompactSpace M] [T2Space M] {x : M} (V : TopologicalSpace.Opens M) (hx : x ∈ V) : ∃ (U : TopologicalSpace.Opens M), x ∈ U ∧ U ≤ V ∧ IsCompact (closure ↑U)

The shrinking lemma: in a locally compact Hausdorff space a point of an open set V has an open neighbourhood inside V with compact closure — the interior of a compact neighbourhood inside V (exists_compact_subset). Internal.

theorem Hironaka.Manifold.BEDanFamStar.exists_diffeomorph_last_of_commutes_injective {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (hcomm : ∀ (m : ℕ), AnalyticFamilyFunctor.CommutesWithLocalIsos (bed.fam m)) {n : ℕ} {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (hinj : Function.Injective ⇑g) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hTT' : T'.IsPullbackOf T g) (hT : DomBEDan 𝕜 T) (hT' : DomBEDan 𝕜 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : ∃ (G : Diffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ((((bed.fam n).fam T' hT').seqOn U' hU').stage (Fin.last (((bed.fam n).fam T' hT').seqOn U' hU').length)).carrier ((((bed.fam n).fam T hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).stage (Fin.last (((bed.fam n).fam T hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).length)).carrier ⊤), (∀ (p : ((((bed.fam n).fam T' hT').seqOn U' hU').stage (Fin.last (((bed.fam n).fam T' hT').seqOn U' hU').length)).carrier), (M.inclusion (AnalyticMap.imageOpens g hg U')) ((((bed.fam n).fam T hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).toSuccession.composite (G p)) = g ((N.inclusion U') ((((bed.fam n).fam T' hT').seqOn U' hU').toSuccession.composite p))) ∧ (((bed.fam n).fam T' hT').seqOn U' hU').toSuccession.strictTransformSubspaceSeq (T'.I.restrict U') (Fin.last (((bed.fam n).fam T' hT').seqOn U' hU').toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G ⋯ ((((bed.fam n).fam T hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).toSuccession.strictTransformSubspaceSeq (T.I.restrict (AnalyticMap.imageOpens g hg U')) (Fin.last (((bed.fam n).fam T hT).seqOn (AnalyticMap.imageOpens g hg U') ⋯).toSuccession.length))

The commutation with local analytic isomorphisms ([Kol07, 34.1]) at an INJECTIVE local analytic isomorphism — the same-model content of the dimension cast exists_diffeomorph_last_of_cast without the cast, g injective instead of a diffeomorphism: for a family functor commuting with local analytic isomorphisms, triples T on M, T' on N with T' the pull-back data of T along g, and a relatively compact open U' of N, the last stages of the values on U' and on g(U') are diffeomorphic over g, and the final strict transforms correspond. The argument: the commutation puts the value on U' in the form ((value on g(U')).pullback (g|U')).eraseEmpty, g|U' : U' → g(U') is a bijective local isomorphism (surjective_restrictMap, injectivity of g), and BlowUpSequence.exists_diffeomorph_last_of_pullback_eraseEmpty closes.

theorem Hironaka.Manifold.exists_padded_equivalence_hom_point {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (x : ↑↑(X.restrictSet V).toPresheafedSpace) : ∃ (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (g : AnalyticMap ((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁) ((pieceAmbient 𝕜 (E₂.padRight n).G).restrict W₂)), (E₁.padLeft m).ambientPoint x ∈ W₁ ∧ IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ ⇑g ∧ Function.Bijective ⇑g ∧ (∃ (hI : (E₁.padLeft m).restrictedIdeal W₁ = Manifold.IdealSheaf.pullback ⇑g ⋯ ((E₂.padRight n).restrictedIdeal W₂)), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑g ⋯ hI) ((E₂.padRight n).restrictedIdealHom W₂)) (E₂.padRight n).embInv = CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdealHom W₁) (E₁.padLeft m).embInv) ∧ ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : (E₁.padLeft m).ambientPoint y ∈ W₁), ↑(g ⟨(E₁.padLeft m).ambientPoint y, hy⟩) = (E₂.padRight n).ambientPoint y

Lemma 39 at the morphism level, with its point clause ([Kol07, Lemma 39]): exists_padded_equivalence_hom (the shear g with the ideal identity and the morphism identity) together with embeddings_equivalent_under_automorphism_pad's point clause — g carries the left-padded ambient points to the right-padded ones — for the SAME witnesses (the shear shearAmbient of the two local lifts). Needed below: that the point s₂(i₂ x) lies in V₂ is read through g at s₁(i₁ x).

theorem Hironaka.Manifold.PieceEmbedding.domBEDan_ambientTriple_pullback_inclusion {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : DomBEDan 𝕜 (E.ambientTriple.pullback ((pieceAmbient 𝕜 E.G).inclusion W) ⋯)

The restricted triple (G, 𝓘_Y, ∅)|_W lies in the class DomBEDan: empty divisor, and the restricted ideal is reduced (isReduced_pullback_of_isLocalDiffeomorph at the open inclusion).

theorem Hironaka.Manifold.PieceEmbedding.localResolutionToPiece_comp_homOfPullbackEq_of_shear {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (bed : BEDanFamStar 𝕜) (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (g : AnalyticMap ((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁) ((pieceAmbient 𝕜 (E₂.padRight n).G).restrict W₂)) (hloc : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ ⇑g) (hI : (E₁.padLeft m).restrictedIdeal W₁ = Manifold.IdealSheaf.pullback ⇑g ⋯ ((E₂.padRight n).restrictedIdeal W₂)) (hmor : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑g ⋯ hI) ((E₂.padRight n).restrictedIdealHom W₂)) (E₂.padRight n).embInv = CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdealHom W₁) (E₁.padLeft m).embInv) (U' : TopologicalSpace.Opens ((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁).carrier) (hU' : IsCompact (closure ↑U')) (G₁ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ((((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.stage (Fin.last (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.length)).carrier (((E₁.padLeft m).localResolutionSeq bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯).toSuccession.stage (Fin.last ((E₁.padLeft m).localResolutionSeq bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯).toSuccession.length)).carrier ⊤) (hG₁sq : ∀ (p : ((((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.stage (Fin.last (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.length)).carrier), ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U')) (((E₁.padLeft m).localResolutionSeq bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯).toSuccession.composite (G₁ p)) = ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ((((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁).inclusion U') ((((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.composite p))) (hG₁id : (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.strictTransformSubspaceSeq (((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯).I.restrict U') (Fin.last (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G₁ ⋯ (((E₁.padLeft m).localResolutionSeq bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯).toSuccession.strictTransformSubspaceSeq ((E₁.padLeft m).restrictedIdeal (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U')) (Fin.last ((E₁.padLeft m).localResolutionSeq bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯).toSuccession.length))) (G₂ : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ((((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.stage (Fin.last (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.length)).carrier (((E₂.padRight n).localResolutionSeq bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯).toSuccession.stage (Fin.last ((E₂.padRight n).localResolutionSeq bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯).toSuccession.length)).carrier ⊤) (hG₂sq : ∀ (p : ((((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.stage (Fin.last (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.length)).carrier), ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U')) (((E₂.padRight n).localResolutionSeq bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯).toSuccession.composite (G₂ p)) = (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ((((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁).inclusion U') ((((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.composite p))) (hG₂id : (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.strictTransformSubspaceSeq (((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯).I.restrict U') (Fin.last (((bed.fam (n + m)).fam ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯) ⋯).seqOn U' hU').toSuccession.length) = Manifold.IdealSheaf.pullback ⇑G₂ ⋯ (((E₂.padRight n).localResolutionSeq bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯).toSuccession.strictTransformSubspaceSeq ((E₂.padRight n).restrictedIdeal (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U')) (Fin.last ((E₂.padRight n).localResolutionSeq bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯).toSuccession.length))) : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑G₂ ⋯ hG₂id) ((E₂.padRight n).localResolutionToPiece bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯) = CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑G₁ ⋯ hG₁id) ((E₁.padLeft m).localResolutionToPiece bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯)

The compatibility Π₂ ∘ m₂ = Π₁ ∘ m₁ over the piece (factored out of exists_isIso_localResolution_of_shear_core), for ANY two last-stage diffeomorphisms G₁ : M' ≃ M₁, G₂ : M' ≃ M₂ from the value on W₁|U' lying over ι₁ and over ι₂ ∘ g (the squares hG₁sq, hG₂sq) and carrying the final strict transform (hG₁id, hG₂id) — the isomorphisms m₁ := homOfPullbackEq G₁, m₂ := homOfPullbackEq G₂. The identity is read after the isomorphism E₁.emb through the shear's morphism identity on W₁, the quotient-map squares (toAnalyticSpaceι_comp_restrictedIdealHom, localResolutionMap_comp_ι, homOfPullbackEq_comp_toAnalyticSpaceι) and the two squares of composites (Hom.ext_of_comp_quotientι, ofManifoldHom_comp/_congr). The core obtains G₁, G₂ from exists_diffeomorph_last_of_commutes_injective.

theorem Hironaka.Manifold.PieceEmbedding.exists_isIso_localResolution_of_shear_core {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (g : AnalyticMap ((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁) ((pieceAmbient 𝕜 (E₂.padRight n).G).restrict W₂)) (hloc : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ ⇑g) (hbij : Function.Bijective ⇑g) (hI : (E₁.padLeft m).restrictedIdeal W₁ = Manifold.IdealSheaf.pullback ⇑g ⋯ ((E₂.padRight n).restrictedIdeal W₂)) (hmor : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑g ⋯ hI) ((E₂.padRight n).restrictedIdealHom W₂)) (E₂.padRight n).embInv = CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdealHom W₁) (E₁.padLeft m).embInv) (U' : TopologicalSpace.Opens ((pieceAmbient 𝕜 (E₁.padLeft m).G).restrict W₁).carrier) (hU' : IsCompact (closure ↑U')) : ∃ (ψ : (E₁.padLeft m).localResolution bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯ ⟶ (E₂.padRight n).localResolution bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ ((E₂.padRight n).localResolutionToPiece bed (AnalyticMap.imageOpens (ContMDiffMap.comp ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) g) ⋯ U') ⋯) = (E₁.padLeft m).localResolutionToPiece bed (AnalyticMap.imageOpens ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯ U') ⋯

The shear's isomorphism of the padded local resolutions over U₁ := ι₁(U') and U₂ := (ι₂ ∘ g)(U') ([Kol07, Theorem 36, proof]: Lemma 39 with the commutation with smooth morphisms), for a relatively compact open U' of the shear's source W₁: the commutation of IsEmbeddedDesing with local isomorphisms along the two injective local isomorphisms ι₁ : W₁ ↪ A₁ and ι₂ ∘ g : W₁ → A₂ at the SAME U' (exists_diffeomorph_last_of_commutes_injective, twice) gives the two last-stage diffeomorphisms G₁, G₂ from the value on W₁|U'; homOfPullbackEq makes them isomorphisms m₁ : Ỹ' ≅ Ỹ₁, m₂ : Ỹ' ≅ Ỹ₂ of the final strict transforms and ψ := m₂ ∘ m₁⁻¹; the compatibility over the piece reduces to Π₂ ∘ m₂ = Π₁ ∘ m₁ (localResolutionToPiece_comp_homOfPullbackEq_of_shear).

theorem Hironaka.Manifold.PieceEmbedding.exists_isIso_localResolution_of_shear' {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (x : ↑↑(X.restrictSet V).toPresheafedSpace) (V₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (hx₁ : (E₁.padLeft m).ambientPoint x ∈ V₁) (V₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (hx₂ : (E₂.padRight n).ambientPoint x ∈ V₂) : ∃ (U₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (hU₁ : IsCompact (closure ↑U₁)) (U₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (hU₂ : IsCompact (closure ↑U₂)), (E₁.padLeft m).ambientPoint x ∈ U₁ ∧ (E₂.padRight n).ambientPoint x ∈ U₂ ∧ U₁ ≤ V₁ ∧ U₂ ≤ V₂ ∧ ∃ (ψ : (E₁.padLeft m).localResolution bed U₁ hU₁ ⟶ (E₂.padRight n).localResolution bed U₂ hU₂), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ ((E₂.padRight n).localResolutionToPiece bed U₂ hU₂) = (E₁.padLeft m).localResolutionToPiece bed U₁ hU₁

The shear's isomorphism with the point clause on the right: the shrunken open U₂ of the right-padded ambient also contains s₂(i₂ x) — the point clause of exists_padded_equivalence_hom_point read at U₂ := (ι₂ ∘ g)(U'), U' ∋ s₁(i₁ x). Used by localResolution_independent_local, whose open N of the piece must lie over BOTH shrunken opens. The argument: exists_padded_equivalence_hom_point, the shrinking lemma inside ι₁⁻¹ V₁ ∩ (ι₂ ∘ g)⁻¹ V₂ around s₁(i₁ x), the core.

theorem Hironaka.Manifold.exists_isIso_localResolution_of_shear {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (x : ↑↑(X.restrictSet V).toPresheafedSpace) (V₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (hx₁ : (E₁.padLeft m).ambientPoint x ∈ V₁) (V₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (hx₂ : (E₂.padRight n).ambientPoint x ∈ V₂) : ∃ (U₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₁.padLeft m).G).carrier) (hU₁ : IsCompact (closure ↑U₁)) (U₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (E₂.padRight n).G).carrier) (hU₂ : IsCompact (closure ↑U₂)), (E₁.padLeft m).ambientPoint x ∈ U₁ ∧ U₁ ≤ V₁ ∧ U₂ ≤ V₂ ∧ ∃ (ψ : (E₁.padLeft m).localResolution bed U₁ hU₁ ⟶ (E₂.padRight n).localResolution bed U₂ hU₂), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ ((E₂.padRight n).localResolutionToPiece bed U₂ hU₂) = (E₁.padLeft m).localResolutionToPiece bed U₁ hU₁

The shear's isomorphism of padded resolutions on shrunken opens (Kol07, Theorem 36, proof): near x, relatively compact opens U₁ ∋ s₁(i₁ x) and U₂ of the padded ambients, inside any prescribed neighbourhoods V₁, V₂, whose local resolutions are isomorphic over the piece — exists_isIso_localResolution_of_shear' without its right point clause.

theorem Hironaka.Manifold.localResolution_independent_local (𝕜 : Type) [RCLike 𝕜] {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {n m : ℕ} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 E₁.G).carrier) (hW₁ : IsCompact (closure ↑W₁)) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 E₂.G).carrier) (hW₂ : IsCompact (closure ↑W₂)) (x : ↑↑(X.restrictSet V).toPresheafedSpace) (hx₁ : x ∈ E₁.embPreimage W₁) (hx₂ : x ∈ E₂.embPreimage W₂) : ∃ (N : Set ↑↑(X.restrictSet V).toPresheafedSpace), IsOpen N ∧ x ∈ N ∧ N ⊆ E₁.embPreimage W₁ ∩ E₂.embPreimage W₂ ∧ ∃ (ψ : (E₁.localResolution bed W₁ hW₁).restrictSet (↑(E₁.localResolutionToPiece bed W₁ hW₁) ⁻¹' N) ⟶ (E₂.localResolution bed W₂ hW₂).restrictSet (↑(E₂.localResolutionToPiece bed W₂ hW₂) ⁻¹' N)), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (AnalyticSpace.Hom.restrictSet (E₂.localResolutionToPiece bed W₂ hW₂) N) = AnalyticSpace.Hom.restrictSet (E₁.localResolutionToPiece bed W₁ hW₁) N

The local independence of the embedding ([Kol07, Theorem 36, proof]; Wlo09, §4, (3)⇒(4)): near every point x of the piece over W₁ and over W₂, an open N ∋ x of the piece over both, over which the local resolutions of the two embeddings are isomorphic compatibly with the maps to the piece. The three legs of Kollár's proof in the relation "isomorphic over N", composed by exists_restrictSet_isIso_trans/_symm: (γ) from W₁ down to W₁' := s₁⁻¹ U₁ (exists_restrictSet_isIso_localResolution_of_le), (α) at the left padding (exists_isIso_localResolution_padAlong, through exists_restrictSet_isIso_of_comp_eq), (β) the shear between the two paddings on the shrunken opens U₁ ∋ s₁(i₁ x), U₂ ∋ s₂(i₂ x) inside p₁⁻¹ W₁, p₂⁻¹ W₂ (exists_isIso_localResolution_of_shear'), (α) at the right padding, (γ) back up from W₂' := s₂⁻¹ U₂ to W₂; N := (E₁ over W₁') ∩ (E₂ over W₂'). The global form is localResolution_independent_of_local (LocalResolutionIndependent.lean).