The inverse piece embeddings under padding and restriction

Four squares of morphisms of closed subspaces, closed by Hom.ext_of_comp_quotientι (a map into a quotient is determined by its composite with the quotient's inclusion) except the third, which follows from the retraction identities of the embeddings (emb_comp_embInv_padAlong, embInv_comp_emb); the final composite square is assembled from the other three:

• homOfPullbackEq along a composite of local analytic isomorphisms is the composite of the homOfPullbackEqs (functoriality of the induced morphism of closed subspaces);
• the padded-slice morphism padSliceHom commutes with the inclusions of ambients (the coordinate square padCoordProj_comp_pieceAmbientIncl of PadRestrict.lean);
• the inverse embedding of the padded piece is the slice morphism followed by the inverse embedding of the piece (emb_comp_embInv_padAlong);
• the inverse embedding of the restricted piece lies over the inclusion of the pieces (restrictPiece_emb_comp_quotientι_comp_ambientInclHom), and so, composing, the inverse embedding of the PADDED RESTRICTED piece is carried by homOfPullbackEq along the padded inclusion of ambients to the inverse embedding of the padded piece, over the inclusion of the pieces.

The last identity is what the transition between a padded piece and a piece of the other embedding needs (ShearOverX.lean): the two read-down maps from the common closed subspace Sp(𝓘₀|W₁') to X are the shear's two maps (hmor) conjugated by these squares. Not in the sources; bookkeeping.

theorem Manifold.IdealSheaf.homOfPullbackEq_comp {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A₁ A₂ A₃ : AnalyticManifold 𝕜 (Fin n → 𝕜)} (f₁ : AnalyticMap A₁ A₂) (f₂ : AnalyticMap A₂ A₃) {J₁ : A₁.IdealSheaf} {J₂ : A₂.IdealSheaf} {J₃ : A₃.IdealSheaf} (h₁ : J₁ = pullback ⇑f₁ ⋯ J₂) (h₂ : J₂ = pullback ⇑f₂ ⋯ J₃) (h₁₂ : J₁ = pullback (⇑f₂ ∘ ⇑f₁) ⋯ J₃) : CategoryTheory.CategoryStruct.comp (homOfPullbackEq ⇑f₁ ⋯ h₁) (homOfPullbackEq ⇑f₂ ⋯ h₂) = homOfPullbackEq (⇑f₂ ∘ ⇑f₁) ⋯ h₁₂

homOfPullbackEq along a composite is the composite of the homOfPullbackEqs — both lie over Sp(f₂ ∘ f₁) (Hom.ext_of_comp_quotientι, homOfPullbackEq_comp_toAnalyticSpaceι, ofManifoldHom_comp).

theorem Hironaka.Manifold.padSliceHom_comp_homOfPullbackEq_pieceAmbientIncl {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G' G : TopologicalSpace.Opens (Fin n → 𝕜)} (h : G' ≤ G) (J : (pieceAmbient 𝕜 G).IdealSheaf) : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑(pieceAmbientIncl ⋯) ⋯ ⋯) (padSliceHom σ J) = CategoryTheory.CategoryStruct.comp (padSliceHom σ (Manifold.IdealSheaf.pullback ⇑(pieceAmbientIncl h) ⋯ J)) (Manifold.IdealSheaf.homOfPullbackEq ⇑(pieceAmbientIncl h) ⋯ ⋯)

The padded-slice morphism commutes with the inclusions of ambients — padSliceHom for J after homOfPullbackEq along the padded inclusion is homOfPullbackEq along the inclusion after padSliceHom for the restricted ideal; both lie over the coordinate square padCoordProj ∘ ι⁺ = ι ∘ padCoordProj'.

theorem Hironaka.Manifold.PieceEmbedding.embInv_padAlong {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {n' : ℕ} (σ : Fin n ↪ Fin n') : (E.padAlong σ).embInv = CategoryTheory.CategoryStruct.comp (padSliceHom σ E.ideal) E.embInv

The inverse embedding of the padded piece is the slice morphism followed by the piece's inverse embedding — emb_comp_embInv_padAlong read backwards through embInv_comp_emb.

theorem Hironaka.Manifold.PieceEmbedding.embInv_comp_homOfPullbackEq_restrictPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V V' : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (hV' : IsOpen V') (hsub : V' ⊆ V) : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑(pieceAmbientIncl ⋯) ⋯ ⋯) E.embInv = CategoryTheory.CategoryStruct.comp (E.restrictPiece hV' hsub).embInv (have this := X.restrictIncl ⋯; this)

The inverse embedding of the restricted piece lies over the inclusion of the pieces — homOfPullbackEq along the inclusion of the shrunk ambient followed by the piece's inverse embedding is the restricted piece's inverse embedding followed by X|V' → X|V (restrictPiece_emb_comp_quotientι_comp_ambientInclHom, Hom.ext_of_comp_quotientι).

theorem Hironaka.Manifold.PieceEmbedding.embInv_comp_homOfPullbackEq_padAlong_restrictPiece {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V V' : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (hV' : IsOpen V') (hsub : V' ⊆ V) {n' : ℕ} (σ : Fin n ↪ Fin n') : CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑(pieceAmbientIncl ⋯) ⋯ ⋯) (E.padAlong σ).embInv = CategoryTheory.CategoryStruct.comp ((E.restrictPiece hV' hsub).padAlong σ).embInv (have this := X.restrictIncl ⋯; this)

The inverse embedding of the padded restricted piece is carried to the inverse embedding of the padded piece by homOfPullbackEq along the padded inclusion of ambients (isPullbackOf_ambientTriple_padAlong_restrictPiece, PadRestrict.lean), over the inclusion of the pieces X|V' → X|V — the pad square, the restrict square and embInv_padAlong twice.