Lemma 39 at the morphism level: the padded embeddings are equivalent as closed subspaces

Kollár's Lemma 39 says that two closed embeddings i₁ : Y → G₁ ⊆ 𝕜ⁿ, i₂ : Y → G₂ ⊆ 𝕜ᵐ of one piece Y = X|V become "equivalent under a (nonlinear) automorphism" after padding to 𝕜^{n+m} [Kol07, Lemma 39]. PieceLemma39Shear.lean proves this on POINTS and IDEALS: the shear Ψ of the two local lifts carries the left-padded embedded points to the right-padded ones and pulls the right-padded ideal back to the left-padded one. The comparison of the local resolutions of a piece for two embeddings [Kol07, Theorem 36, proof] needs the statement as an identity of MORPHISMS: the isomorphism of closed subspaces Sp(W₁)/𝓘₁|W₁ ≅ Sp(W₂)/𝓘₂|W₂ induced by the shear (the functoriality of the closed subspace along Sp(Ψ), ClosedSubspaceHom.lean's homOfPullbackEq), read down to X|V through the two paddings, is the identity of the piece. The point clause alone does not determine the stalk maps: over ℝ, the ideal (x² + y²) on 𝕜² admits the automorphism y ↦ −y of the padded ambient fixing the embedded points. This module proves that identity, exists_padded_equivalence_hom.

The mathematics is that of the shear module: the padded stalk maps of the two embeddings agree through the shear (padStalkMap_eq_comp_germMapOn_shear), and a morphism into Sp(M) is determined by its action on coordinate germs (hom_ext_of_coord_chart, Hironaka/AnalyticSpace/MonoidalUnique.lean). The argument:

• the padding links — padSliceIso_inv_eq_homOfPullbackEq (the inverse of the slice isomorphism padSliceIso of PadIdeal.lean is the closed-subspace morphism over the zero extension s, a right inverse of padSliceHom because p ∘ s = id), PieceEmbedding.toAnalyticSpaceι_comp_padAlong_emb (the padded ambient embedding lies over s), toAnalyticSpaceι_comp_restrictedIdealHom (the restriction-of-a-quotient map restrictedIdealHom of PieceIndependence.lean, the closed-subspace morphism over the open inclusion, lies over it);
• the points — PieceEmbedding.exists_ambientPoint_eq_of_stalkIdeal_ne_top (the cosupport of the ideal is the set of embedded points), toFun_embInv_restrictedIdealHom (the read-down map emb⁻¹ ∘ restrictedIdealHom W on points), ambient_comp_embInv_restrictedIdealHom (the read-down map followed by the ambient embedding is the inclusion of the closed subspace);
• the core — padded_equivalence_hom_aux and padded_equivalence_hom_of_stalkMap: for ANY local isomorphism Ψ of the padded ambients restricting to a diffeomorphism W₁ ≃ W₂ that carries the embedded points and interchanges the padded stalk maps, the morphism identity; the proof cancels the isomorphism emb₂ and the closed-subspace inclusion toAnalyticSpaceι (Hom.ext_of_comp_quotientι), then compares two morphisms Sp(W₁)/𝓘₁|W₁ ⟶ Sp(padOpens₂) on coordinate germs: at a point over the embedded point s₁(i₁ y) the germs pull back equally by the stalk identity, the two composite stalk maps being identified as MORPHISM identities (stalkMap_germ_congr transporting the germ of the section u_j ∘ Ψ, no dependent rewrite);
• the assembly — padded_equivalence_hom_of_shear (the core at the shear of the two lifts) and exists_padded_equivalence_hom: the witnesses of embeddings_equivalent_under_automorphism_pad, the ideal identity pullback_padIdeal_inclusion_eq_of_shear (the shear module's extracted fourth clause) and the morphism identity.

Not in the sources beyond Lemma 39; bookkeeping over the shear module. The theorem itself has no user in the library: exists_padded_equivalence_hom_point (LocalResolutionShear.lean) repeats its construction with the point clause of embeddings_equivalent_under_automorphism_pad added, on the same witnesses, and that form is what LocalResolutionShear.lean and CoproductMixedTransition.lean use; the core padded_equivalence_hom_of_shear is shared by both.

The padding links

theorem Hironaka.Manifold.padSliceIso_inv_eq_homOfPullbackEq {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : (padSliceIso σ J).inv = Manifold.IdealSheaf.homOfPullbackEq (padExt σ G) ⋯ ⋯

The inverse of the slice isomorphism padSliceIso is the closed-subspace morphism over the zero extension s = padExt (homOfPullbackEq at s, with s^*(p^*J + 𝓘_S) = J, pullback_padExt_padIdeal): it is a right inverse of padSliceHom because p ∘ s = id (padCoordProj_padExt, ofManifoldHom_comp, Hom.ext_of_comp_quotientι), and a right inverse of an isomorphism is its inverse (IsIso.eq_inv_of_inv_hom_id).

theorem Hironaka.Manifold.PieceEmbedding.toAnalyticSpaceι_comp_padAlong_emb {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {n' : ℕ} (σ : Fin n ↪ Fin n') : CategoryTheory.CategoryStruct.comp (E.padAlong σ).emb (E.padAlong σ).ideal.toAnalyticSpaceι = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp E.emb E.ideal.toAnalyticSpaceι) (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom (padExt σ E.G) ⋯; this)

The padded ambient embedding lies over the zero extension (the padding 𝕜ⁿ ⊂ 𝕜ⁿ⁺ᵐ of [Kol07, Theorem 36, proof]; compare [Wlo09, §7.1]): ι' ∘ emb' = Sp(s) ∘ ι ∘ emb for the padding E.padAlong σ — its emb is (padSliceIso σ 𝓘)⁻¹ ∘ emb, so padSliceIso_inv_eq_homOfPullbackEq and homOfPullbackEq_comp_toAnalyticSpaceι.

theorem Hironaka.Manifold.PieceEmbedding.toAnalyticSpaceι_comp_restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : CategoryTheory.CategoryStruct.comp (E.restrictedIdealHom W) E.ideal.toAnalyticSpaceι = CategoryTheory.CategoryStruct.comp (E.restrictedIdeal W).toAnalyticSpaceι (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom ⇑((pieceAmbient 𝕜 E.G).inclusion W) ⋯; this)

The restriction-of-a-quotient map lies over the open inclusion, as morphisms Sp(W)/𝓘|W ⟶ Sp(G): the morphism form of toFun_toAnalyticSpaceι_restrictedIdealHom (homOfPullbackEq_comp_toAnalyticSpaceι at the open inclusion).

theorem Hironaka.Manifold.PieceEmbedding.exists_ambientPoint_eq_of_stalkIdeal_ne_top {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (z : (pieceAmbient 𝕜 E.G).carrier) (hz : Manifold.IdealSheaf.stalkIdeal E.ideal z ≠ ⊤) : ∃ (y : ↑↑(X.restrictSet V).toPresheafedSpace), E.ambientPoint y = z

The embedded points are the cosupport of the ideal: a point of G with a proper stalk of 𝓘_Y is an ambient point i(y) — the contrapositive of stalkIdeal_eq_top_of_forall_ne.

theorem Hironaka.Manifold.PieceEmbedding.toFun_embInv_restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (z : ↑↑(E.restrictedIdeal W).toAnalyticSpace.toPresheafedSpace) {y : ↑↑(X.restrictSet V).toPresheafedSpace} (hy : E.ambientPoint y = ↑(↑(E.restrictedIdeal W).toAnalyticSpaceι z)) : ↑(CategoryTheory.CategoryStruct.comp (E.restrictedIdealHom W) E.embInv) z = y

The read-down map on points: a point z of Sp(W)/𝓘|W lying over the ambient point i(y) is carried by emb⁻¹ ∘ restrictedIdealHom W to y (Subtype.ext on Sp(G)/𝓘, then embInv_comp_emb).

theorem Hironaka.Manifold.PieceEmbedding.ambient_comp_embInv_restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (E.restrictedIdealHom W) E.embInv) (CategoryTheory.CategoryStruct.comp E.emb E.ideal.toAnalyticSpaceι) = CategoryTheory.CategoryStruct.comp (E.restrictedIdeal W).toAnalyticSpaceι (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom ⇑((pieceAmbient 𝕜 E.G).inclusion W) ⋯; this)

The read-down map, followed by the ambient embedding, is the inclusion of the closed subspace: (ι ∘ emb) ∘ (emb⁻¹ ∘ restrictedIdealHom W) = Sp(W ↪ G) ∘ ι_W (emb_comp_embInv, toAnalyticSpaceι_comp_restrictedIdealHom).

The core identity from the stalk identity

theorem Hironaka.Manifold.padded_equivalence_hom_aux {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) (Gd : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict W₁).carrier ((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).restrict W₂).carrier ⊤) (Ψ : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier → (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) (hΨ : ContMDiffOn (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ Ψ ↑W₁) (hg : ∀ (z : ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict W₁).carrier), ↑(Gd z) = Ψ ↑z) (hpt : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ W₁ → Ψ (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)) (hδ : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hb : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ W₁) (hc : Ψ (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)), padStalkMap E₂ (Fin.natAddEmb n) y = (padStalkMap E₁ (Fin.castAddEmb m) y).comp (Manifold.germMapOn Ψ hΨ hb hc)) : CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdeal W₁).toAnalyticSpaceι (CategoryTheory.CategoryStruct.comp (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom ⇑↑Gd ⋯; this) (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom ⇑((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).inclusion W₂) ⋯; this)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdealHom W₁) (E₁.padLeft m).embInv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp E₂.emb E₂.ideal.toAnalyticSpaceι) (have this := AnalyticSpace.KLocallyRingedSpace.ofManifoldHom (padExt (Fin.natAddEmb n) E₂.G) ⋯; this))

The coordinate-germ step of the core: the two morphisms Sp(W₁)/𝓘₁|W₁ ⟶ Sp(padOpens₂) — the inclusion after g, and the right-padded ambient embedding after the read-down map — are equal: hom_ext_of_coord_chart at every point, the coordinate germs pulled back equally by the stalk identity hδ.

theorem Hironaka.Manifold.padded_equivalence_hom_of_stalkMap {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) (Gd : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict W₁).carrier ((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).restrict W₂).carrier ⊤) (Ψ : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier → (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) (hΨ : ContMDiffOn (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ Ψ ↑W₁) (hg : ∀ (z : ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict W₁).carrier), ↑(Gd z) = Ψ ↑z) (hpt : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ W₁ → Ψ (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)) (hδ : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hb : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ W₁) (hc : Ψ (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)), padStalkMap E₂ (Fin.natAddEmb n) y = (padStalkMap E₁ (Fin.castAddEmb m) y).comp (Manifold.germMapOn Ψ hΨ hb hc)) (hI : (E₁.padLeft m).restrictedIdeal W₁ = Manifold.IdealSheaf.pullback ⇑↑Gd ⋯ ((E₂.padRight n).restrictedIdeal W₂)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑↑Gd ⋯ hI) ((E₂.padRight n).restrictedIdealHom W₂)) (E₂.padRight n).embInv = CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdealHom W₁) (E₁.padLeft m).embInv

The core in general form: the morphism identity from the stalk identity, for any local isomorphism Ψ of the padded ambients restricting to a diffeomorphism Gd : W₁ ≃ W₂, carrying the left-padded embedded points to the right-padded ones and interchanging the padded stalk maps.

The core identity at the shear of the two lifts, and the assembly

theorem Hironaka.Manifold.padded_equivalence_hom_of_shear {𝕜 : 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) (O₁ : TopologicalSpace.Opens (Fin n → 𝕜)) (j₂ : (Fin n → 𝕜) → Fin m → 𝕜) (hj₂ : ContDiffOn 𝕜 ⊤ j₂ ↑O₁) (O₂ : TopologicalSpace.Opens (Fin m → 𝕜)) (j₁ : (Fin m → 𝕜) → Fin n → 𝕜) (hj₁ : ContDiffOn 𝕜 ⊤ j₁ ↑O₂) (v₂ : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), E₁.modelPoint y ∈ O₁ → j₂ (E₁.modelPoint y) = E₂.modelPoint y) (v₁ : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), E₂.modelPoint y ∈ O₂ → j₁ (E₂.modelPoint y) = E₁.modelPoint y) (H₂ : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : E₁.modelPoint y ∈ O₁) (k : Fin m), (E₂.modelStalkMap y) (modelCoordGerm (E₂.modelPoint y) k) = (E₁.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => j₂ v k) ⋯ hy)) (H₁ : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : E₂.modelPoint y ∈ O₂) (k : Fin n), (E₁.modelStalkMap y) (modelCoordGerm (E₁.modelPoint y) k) = (E₂.modelStalkMap y) (modelGerm (fun (v : Fin m → 𝕜) => j₁ v k) ⋯ hy)) (hI : (E₁.padLeft m).restrictedIdeal { carrier := (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source, is_open' := ⋯ } = Manifold.IdealSheaf.pullback ⇑↑(partialDiffeomorphToDiffeomorph (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁)) ⋯ ((E₂.padRight n).restrictedIdeal { carrier := (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).target, is_open' := ⋯ })) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Manifold.IdealSheaf.homOfPullbackEq ⇑↑(partialDiffeomorphToDiffeomorph (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁)) ⋯ hI) ((E₂.padRight n).restrictedIdealHom { carrier := (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).target, is_open' := ⋯ })) (E₂.padRight n).embInv = CategoryTheory.CategoryStruct.comp ((E₁.padLeft m).restrictedIdealHom { carrier := (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source, is_open' := ⋯ }) (E₁.padLeft m).embInv

The morphism identity for the explicit shear Ψ = shearAmbient of the two lifts ([Kol07, Lemma 39, proof]): with W₁ := Ψ.source, W₂ := Ψ.target, g := Ψ restricted and hI the ideal identity (pullback_padIdeal_inclusion_eq_of_shear), the closed-subspace morphism homOfPullbackEq over g, read down to X|V through the right padding, is the left padding's reading — the general core padded_equivalence_hom_of_stalkMap at the shear: the embedded points are carried by shearAmbient_padExt, the padded stalk maps interchanged by padStalkMap_eq_comp_germMapOn_shear.

theorem Hironaka.Manifold.exists_padded_equivalence_hom {𝕜 : 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

Lemma 39 at the MORPHISM level ([Kol07, Lemma 39]: the two padded embeddings are "equivalent under a (nonlinear) automorphism", built in the proof from an extension j₂ of i₂): near the padded ambient point of every x, a bijective local analytic isomorphism g of opens of the padded ambients pulling the right-padded restricted ideal back to the left-padded one, such that the morphism of closed subspaces Sp(W₁)/𝓘₁|W₁ → Sp(W₂)/𝓘₂|W₂ over g (homOfPullbackEq), followed by the right padding's identification with X|V, is the left padding's identification — the closed-subspace isomorphism induced by the shear IS the identity of the piece. Proved from the local lifts (exists_modelLift, PieceLemma39Model.lean) and the shear shearAmbient of the two lifts: the witnesses of embeddings_equivalent_under_automorphism_pad, the ideal identity pullback_padIdeal_inclusion_eq_of_shear, the morphism identity padded_equivalence_hom_of_shear. The point clause of embeddings_equivalent_under_automorphism is its shadow on base points.