The shear isomorphism of Kollár's Lemma 39, and the equivalence of two embeddings

Kollár's Lemma 39 [Kol07, Lemma 39]: for two closed embeddings i₁ : Y ↪ 𝕜ⁿ, i₂ : Y ↪ 𝕜ᵐ of one piece, the paddings (i₁, 0) and (0, i₂) into 𝕜ⁿ⁺ᵐ are equivalent under a (nonlinear) automorphism. The proof extends i₂ to j₂ : 𝕜ⁿ → 𝕜ᵐ and i₁ to j₁ : 𝕜ᵐ → 𝕜ⁿ and uses the two shears Φ₂ (x, y) = (x, y + j₂ x) and Φ₁ (x, y) = (x + j₁ y, y), each carrying one padding onto the image of (i₁, i₂) [Kol07, Lemma 39, proof]; analytically the extensions exist only locally, so the composite Φ₁⁻¹ ∘ Φ₂ carries the paddings into each other near any point, with the local lifts j₂, j₁ of PieceLemma39Model.lean. This module provides:

• the bookkeeping of partial analytic isomorphisms — membership in the source and target of a composite, the restriction of a partial analytic isomorphism to an analytic isomorphism from its source onto its target (partialDiffeomorphToDiffeomorph);
• the coordinates of the paddings: pieceCoord (padExt σ w) = extend σ (pieceCoord w) 0;
• the shear isomorphism Ψₐ = chart₂⁻¹ ∘ (Φ₂.trans Φ₁.symm) ∘ chart₁ between the two padded ambients, its source and target, and the point condition Ψₐ (i₁(y), 0) = (0, i₂(y)) ;
• the ideal identity at the embedded points (the kernel argument: both stalk ideals are the kernels of the padded stalk maps ε ∘ s^*, which Ψₐ^* interchanges by the coordinate identities of the lifts) and off them (⊤ = ⊤, the embedded points of the two paddings corresponding under Ψₐ);
• the theorem embeddings_equivalent_under_automorphism, the analytic form of Lemma 39.

Włodarczyk's counterpart is the commutation of the resolution of a marked ideal with closed embeddings of the ambient manifold [Wlo09, §7.1]. The proofs are routine.

Partial analytic isomorphisms: composites, sources, targets, restriction

theorem Hironaka.Manifold.partialDiffeomorph_trans_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_5} [TopologicalSpace N] [ChartedSpace E' N] {P : Type u_6} [TopologicalSpace P] [ChartedSpace E'' P] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M N ⊤) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E'') N P ⊤) (z : M) : ↑(Φ.trans Ψ).toPartialEquiv z = ↑Ψ.toPartialEquiv (↑Φ.toPartialEquiv z)

theorem Hironaka.Manifold.partialDiffeomorph_trans_symm_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_5} [TopologicalSpace N] [ChartedSpace E' N] {P : Type u_6} [TopologicalSpace P] [ChartedSpace E'' P] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M N ⊤) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E'') N P ⊤) (w : P) : ↑(Φ.trans Ψ).symm.toPartialEquiv w = ↑Φ.symm.toPartialEquiv (↑Ψ.symm.toPartialEquiv w)

theorem Hironaka.Manifold.mem_partialDiffeomorph_trans_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_5} [TopologicalSpace N] [ChartedSpace E' N] {P : Type u_6} [TopologicalSpace P] [ChartedSpace E'' P] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M N ⊤) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E'') N P ⊤) (z : M) : z ∈ (Φ.trans Ψ).source ↔ z ∈ Φ.source ∧ ↑Φ.toPartialEquiv z ∈ Ψ.source

theorem Hironaka.Manifold.mem_partialDiffeomorph_trans_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_5} [TopologicalSpace N] [ChartedSpace E' N] {P : Type u_6} [TopologicalSpace P] [ChartedSpace E'' P] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M N ⊤) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E'') N P ⊤) (w : P) : w ∈ (Φ.trans Ψ).target ↔ w ∈ Ψ.target ∧ ↑Ψ.symm.toPartialEquiv w ∈ Φ.target

theorem Hironaka.Manifold.mem_partialDiffeomorph_symm_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_5} [TopologicalSpace N] [ChartedSpace E' N] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M N ⊤) (w : N) : w ∈ Φ.symm.source ↔ w ∈ Φ.target

theorem Hironaka.Manifold.mem_partialDiffeomorph_symm_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_5} [TopologicalSpace N] [ChartedSpace E' N] (Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') M N ⊤) (z : M) : z ∈ Φ.symm.target ↔ z ∈ Φ.source

def Hironaka.Manifold.partialDiffeomorphToDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (M.restrict { carrier := Ψ.source, is_open' := ⋯ }).carrier (N.restrict { carrier := Ψ.target, is_open' := ⋯ }).carrier ⊤

A partial analytic isomorphism Ψ : M ⇀ N between analytic manifolds, as an analytic isomorphism from its source onto its target (the restrictions M|source, N|target).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.partialDiffeomorphToDiffeomorph_apply_coe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) (z : (M.restrict { carrier := Ψ.source, is_open' := ⋯ }).carrier) : ↑((partialDiffeomorphToDiffeomorph Ψ) z) = ↑Ψ.toPartialEquiv ↑z

The coordinates of the paddings

noncomputable def Hironaka.Manifold.modelPadExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') : (Fin n → 𝕜) → Fin n' → 𝕜

The zero extension 𝕜ⁿ → 𝕜ⁿ' along σ on the model spaces.

Equations

• Hironaka.Manifold.modelPadExt σ v = Function.extend (⇑σ) v 0

theorem Hironaka.Manifold.contDiff_modelPadExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') : ContDiff 𝕜 ⊤ (modelPadExt σ)

theorem Hironaka.Manifold.contDiffOn_modelPadExt_apply {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (i : Fin n') (O : TopologicalSpace.Opens (Fin n → 𝕜)) : ContDiffOn 𝕜 ⊤ (fun (v : Fin n → 𝕜) => modelPadExt σ v i) ↑O

theorem Hironaka.Manifold.pieceCoord_padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : pieceCoord (padOpens σ G) (padExt σ G w) = modelPadExt σ (pieceCoord G w)

Germs of functions of the model space: congruence, subtraction, coordinates

theorem Hironaka.Manifold.modelGerm_congr {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O O' : TopologicalSpace.Opens (Fin n → 𝕜)} {f g : (Fin n → 𝕜) → 𝕜} (hf : ContDiffOn 𝕜 ⊤ f ↑O) (hg : ContDiffOn 𝕜 ⊤ g ↑O') {v : Fin n → 𝕜} (hv : v ∈ O) (hv' : v ∈ O') (h : ∀ᶠ (w : Fin n → 𝕜) in nhds v, f w = g w) : modelGerm f hf hv = modelGerm g hg hv'

theorem Hironaka.Manifold.modelGerm_sub {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} {f g : (Fin n → 𝕜) → 𝕜} (hf : ContDiffOn 𝕜 ⊤ f ↑O) (hg : ContDiffOn 𝕜 ⊤ g ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) : modelGerm (fun (w : Fin n → 𝕜) => f w - g w) ⋯ hv = modelGerm f hf hv - modelGerm g hg hv

theorem Hironaka.Manifold.modelGerm_zero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} {f : (Fin n → 𝕜) → 𝕜} (hf : ContDiffOn 𝕜 ⊤ f ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) (h : ∀ (w : Fin n → 𝕜), f w = 0) : modelGerm f hf hv = 0

theorem Hironaka.Manifold.modelGerm_eq_modelCoordGerm {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {O : TopologicalSpace.Opens (Fin n → 𝕜)} {f : (Fin n → 𝕜) → 𝕜} (hf : ContDiffOn 𝕜 ⊤ f ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) (k : Fin n) (h : ∀ (w : Fin n → 𝕜), f w = w k) : modelGerm f hf hv = modelCoordGerm v k

theorem Hironaka.Manifold.germMapOn_modelGerm {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {j : (Fin n → 𝕜) → Fin m → 𝕜} {O : TopologicalSpace.Opens (Fin n → 𝕜)} (hj : ContDiffOn 𝕜 ⊤ j ↑O) {v : Fin n → 𝕜} (hv : v ∈ O) {w : Fin m → 𝕜} (hjv : j v = w) {O' : TopologicalSpace.Opens (Fin m → 𝕜)} {f : (Fin m → 𝕜) → 𝕜} (hf : ContDiffOn 𝕜 ⊤ f ↑O') (hw : w ∈ O') {O'' : TopologicalSpace.Opens (Fin n → 𝕜)} (hfj : ContDiffOn 𝕜 ⊤ (f ∘ j) ↑O'') (hv'' : v ∈ O'') : (Manifold.germMapOn j ⋯ hv hjv) (modelGerm f hf hw) = modelGerm (f ∘ j) hfj hv''

The germ map of a partial analytic map carries the model germ of f to the model germ of f ∘ j.

theorem Hironaka.Manifold.germMapOn_partialDiffeomorph_bijective' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M₁' : Type u} [TopologicalSpace M₁'] [ChartedSpace E M₁'] {M₂' : Type u} [TopologicalSpace M₂'] [ChartedSpace E M₂'] (g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤) {x : M₁'} (hx : x ∈ g.source) {c : M₂'} (hc : ↑g.toPartialEquiv x = c) : Function.Bijective ⇑(Manifold.germMapOn ↑g.toPartialEquiv ⋯ hx hc)

The stalk map along a partial analytic isomorphism, read at any point equal to the image, is bijective (germMapOn_partialDiffeomorph_bijective with the target point transported).

The shear automorphism of the model space ([Kol07, Lemma 39, proof])

theorem Hironaka.Manifold.shearFst_append {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O₂ : TopologicalSpace.Opens (Fin m → 𝕜)) (j₁ : (Fin m → 𝕜) → Fin n → 𝕜) (hj₁ : ContDiffOn 𝕜 ⊤ j₁ ↑O₂) (a : Fin n → 𝕜) (b : Fin m → 𝕜) : ↑(shearFst O₂ j₁ hj₁).toPartialEquiv (Fin.append a b) = Fin.append (a + j₁ b) b

The shear (x, y) ↦ (x + j(y), y) of [Kol07, Lemma 39, proof] on a block pair.

def Hironaka.Manifold.shearModel {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (Fin (n + m) → 𝕜) (Fin (n + m) → 𝕜) ⊤

The composite Φ₁⁻¹ ∘ Φ₂ of the two shears of [Kol07, Lemma 39, proof] on the model space 𝕜ⁿ⁺ᵐ: the shear by j₂ in the second block followed by the inverse shear by j₁ in the first.

Equations

• Hironaka.Manifold.shearModel O₁ j₂ hj₂ O₂ j₁ hj₁ = (Hironaka.Manifold.shearSnd O₁ j₂ hj₂).trans (Hironaka.Manifold.shearFst O₂ j₁ hj₁).symm

theorem Hironaka.Manifold.shearModel_apply {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (z : Fin (n + m) → 𝕜) : ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv z = ↑(shearFst O₂ j₁ hj₁).symm.toPartialEquiv (↑(shearSnd O₁ j₂ hj₂).toPartialEquiv z)

theorem Hironaka.Manifold.mem_shearModel_source {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (z : Fin (n + m) → 𝕜) : z ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).source ↔ z ∘ Fin.castAdd m ∈ O₁ ∧ ↑(shearSnd O₁ j₂ hj₂).toPartialEquiv z ∘ Fin.natAdd n ∈ O₂

theorem Hironaka.Manifold.mem_shearModel_target {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (w : Fin (n + m) → 𝕜) : w ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).target ↔ w ∘ Fin.natAdd n ∈ O₂ ∧ ↑(shearFst O₂ j₁ hj₁).toPartialEquiv w ∘ Fin.castAdd m ∈ O₁

theorem Hironaka.Manifold.shearModel_append_zero {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (a : Fin n → 𝕜) : ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (Fin.append a 0) = Fin.append (a - j₁ (j₂ a)) (j₂ a)

Φ₁⁻¹ (Φ₂ (x, 0)) = (x - j₁ (j₂ x), j₂ x).

theorem Hironaka.Manifold.shearModel_append_zero_of_eq {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (a : Fin n → 𝕜) (ha : j₁ (j₂ a) = a) : ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (Fin.append a 0) = Fin.append 0 (j₂ a)

theorem Hironaka.Manifold.append_zero_mem_shearModel_source {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (a : Fin n → 𝕜) (ha : a ∈ O₁) (hb : j₂ a ∈ O₂) : Fin.append a 0 ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).source

theorem Hironaka.Manifold.of_append_zero_mem_shearModel_source {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (a : Fin n → 𝕜) (h : Fin.append a 0 ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).source) : a ∈ O₁ ∧ j₂ a ∈ O₂

theorem Hironaka.Manifold.of_zero_append_mem_shearModel_target {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (b : Fin m → 𝕜) (h : Fin.append 0 b ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).target) : b ∈ O₂ ∧ j₁ b ∈ O₁

The shear isomorphism of the padded ambients

theorem Hironaka.Manifold.pieceCoord_padExt_castAdd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (w : (pieceAmbient 𝕜 E₁.G).carrier) : pieceCoord (padOpens (Fin.castAddEmb m) E₁.G) (padExt (Fin.castAddEmb m) E₁.G w) = Fin.append (pieceCoord E₁.G w) 0

The left-padded ambient point in coordinates, (i(y), 0).

theorem Hironaka.Manifold.pieceCoord_padExt_natAdd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₂ : PieceEmbedding 𝕜 m X V) (w : (pieceAmbient 𝕜 E₂.G).carrier) : pieceCoord (padOpens (Fin.natAddEmb n) E₂.G) (padExt (Fin.natAddEmb n) E₂.G w) = Fin.append 0 (pieceCoord E₂.G w)

The right-padded ambient point in coordinates, (0, i(y)).

theorem Hironaka.Manifold.ambientPoint_padLeft {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : (E₁.padLeft m).ambientPoint y = padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)

theorem Hironaka.Manifold.ambientPoint_padRight {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₂ : PieceEmbedding 𝕜 m X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : (E₂.padRight n).ambientPoint y = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)

noncomputable def Hironaka.Manifold.shearAmbient {𝕜 : 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₂) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier ⊤

The shear of [Kol07, Lemma 39, proof] on the padded ambients: chart₂⁻¹ ∘ (Φ₁⁻¹ ∘ Φ₂) ∘ chart₁ : Sp(G₁ × 𝕜ᵐ) ⇀ Sp(𝕜ⁿ × G₂), the charts being taken at the padded ambient points of x.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.shearAmbient_apply {𝕜 : 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₂) (z : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) : ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv z = ↑(pieceAmbientChart (padOpens (Fin.natAddEmb n) E₂.G) (padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint x))).symm.toPartialEquiv (↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (pieceCoord (padOpens (Fin.castAddEmb m) E₁.G) z))

theorem Hironaka.Manifold.mem_shearAmbient_source {𝕜 : 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₂) (z : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) : z ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source ↔ pieceCoord (padOpens (Fin.castAddEmb m) E₁.G) z ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).source ∧ ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (pieceCoord (padOpens (Fin.castAddEmb m) E₁.G) z) ∈ (pieceAmbientChart (padOpens (Fin.natAddEmb n) E₂.G) (padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint x))).target

theorem Hironaka.Manifold.mem_shearAmbient_target {𝕜 : 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₂) (w : (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) : w ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).target ↔ pieceCoord (padOpens (Fin.natAddEmb n) E₂.G) w ∈ (shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).target ∧ ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).symm.toPartialEquiv (pieceCoord (padOpens (Fin.natAddEmb n) E₂.G) w) ∈ (pieceAmbientChart (padOpens (Fin.castAddEmb m) E₁.G) (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint x))).target

theorem Hironaka.Manifold.shearAmbient_padExt {𝕜 : 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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (h₂ : j₂ (E₁.modelPoint y) = E₂.modelPoint y) (h₁ : j₁ (E₂.modelPoint y) = E₁.modelPoint y) : ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)

The point condition: the shear carries (i₁(y), 0) to (0, i₂(y)) when the lifts take i₁(y) to i₂(y) and back ([Kol07, Lemma 39, proof]).

theorem Hironaka.Manifold.padExt_mem_shearAmbient_source {𝕜 : 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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy₁ : E₁.modelPoint y ∈ O₁) (hy₂ : E₂.modelPoint y ∈ O₂) (h₂ : j₂ (E₁.modelPoint y) = E₂.modelPoint y) (h₁ : j₁ (E₂.modelPoint y) = E₁.modelPoint y) : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source

theorem Hironaka.Manifold.modelPoint_mem_of_padExt_mem_source {𝕜 : 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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (h : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source) : E₁.modelPoint y ∈ O₁ ∧ j₂ (E₁.modelPoint y) ∈ O₂

theorem Hironaka.Manifold.modelPoint_mem_of_padExt_mem_target {𝕜 : 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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (h : padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).target) : E₂.modelPoint y ∈ O₂ ∧ j₁ (E₂.modelPoint y) ∈ O₁

The padded stalk maps and the kernel argument

noncomputable def Hironaka.Manifold.padStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {N : ℕ} (σ : Fin n ↪ Fin N) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : ↑((Manifold.structureSheaf 𝕜 (Fin N → 𝕜) (pieceAmbient 𝕜 (padOpens σ E.G)).carrier).presheaf.stalk (padExt σ E.G (E.ambientPoint y))) →+* ↑((X.restrictSet V).presheaf.stalk y)

The padded stalk map δ = ε ∘ s^* : 𝒪_{𝕜ⁿ' ⊇ G', s(i(y))} →+* 𝒪_{X|V, y} of a piece embedding along a coordinate padding: the stalk map of the piece after the restriction to the slice. Its kernel is the stalk of the padded ideal (stalkIdeal_padIdeal_padExt with stalkIdeal_eq_ker_pieceStalkMap).

Equations

• Hironaka.Manifold.padStalkMap E σ y = (E.pieceStalkMap y).comp (Manifold.germMap (Hironaka.Manifold.padExt σ E.G) ⋯ (E.ambientPoint y))

theorem Hironaka.Manifold.stalkIdeal_padIdeal_eq_ker_padStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {N : ℕ} (σ : Fin n ↪ Fin N) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : Manifold.IdealSheaf.stalkIdeal (padIdeal σ E.ideal) (padExt σ E.G (E.ambientPoint y)) = RingHom.ker (padStalkMap E σ y)

instance Hironaka.Manifold.isLocalHom_padStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {N : ℕ} (σ : Fin n ↪ Fin N) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : IsLocalHom (padStalkMap E σ y)

theorem Hironaka.Manifold.padStalkMap_const {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {N : ℕ} (σ : Fin n ↪ Fin N) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (c : 𝕜) : (padStalkMap E σ y) ((Manifold.const 𝕜 (Fin N → 𝕜) (pieceAmbient 𝕜 (padOpens σ E.G)).carrier (padExt σ E.G (E.ambientPoint y))) c) = ((X.restrictSet V).constAt y) c

theorem Hironaka.Manifold.padStalkMap_coord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {N : ℕ} (σ : Fin n ↪ Fin N) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (i : Fin N) : (padStalkMap E σ y) (Manifold.coord (Fin N → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin N → 𝕜)) (chartAt (Fin N → 𝕜) (padExt σ E.G (E.ambientPoint y))) ⋯ ⋯ i) = (E.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => modelPadExt σ v i) ⋯ ⋯)

The padded stalk map on the coordinate germs of the padded ambient: the i-th coordinate of the zero extension, pulled back through the piece.

def Hironaka.Manifold.shearModelOpens {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) : TopologicalSpace.Opens (Fin n → 𝕜)

The open of 𝕜ⁿ where the shear is defined on the left-padded model points.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.contDiffOn_shearModel_modelPadExt {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (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₂) (i : Fin (n + m)) : ContDiffOn 𝕜 ⊤ (fun (v : Fin n → 𝕜) => ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (modelPadExt (Fin.castAddEmb m) v) i) ↑(shearModelOpens O₁ j₂ hj₂ O₂ j₁ hj₁)

theorem Hironaka.Manifold.padStalkMap_shear_coord {𝕜 : 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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hb : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source) (hc : ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)) (hv : E₁.modelPoint y ∈ shearModelOpens O₁ j₂ hj₂ O₂ j₁ hj₁) (i : Fin (n + m)) : (padStalkMap E₁ (Fin.castAddEmb m) y) ((Manifold.germMapOn ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv ⋯ hb hc) (Manifold.coord (Fin (n + m) → 𝕜) (ContinuousLinearEquiv.refl 𝕜 (Fin (n + m) → 𝕜)) (chartAt (Fin (n + m) → 𝕜) (padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y))) ⋯ ⋯ i)) = (E₁.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => ↑(shearModel O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (modelPadExt (Fin.castAddEmb m) v) i) ⋯ hv)

The padded stalk map of E₁ after the shear, on the coordinate germs of the right-padded ambient: the i-th coordinate of Ψ ∘ s₁, pulled back through E₁.

theorem Hironaka.Manifold.padStalkMap_eq_comp_germMapOn_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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy₁ : E₁.modelPoint y ∈ O₁) (hy₂ : E₂.modelPoint y ∈ O₂) (h₂ : j₂ (E₁.modelPoint y) = E₂.modelPoint y) (H₂ : ∀ (k : Fin m), (E₂.modelStalkMap y) (modelCoordGerm (E₂.modelPoint y) k) = (E₁.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => j₂ v k) ⋯ hy₁)) (H₁ : ∀ (k : Fin n), (E₁.modelStalkMap y) (modelCoordGerm (E₁.modelPoint y) k) = (E₂.modelStalkMap y) (modelGerm (fun (v : Fin m → 𝕜) => j₁ v k) ⋯ hy₂)) (hb : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source) (hc : ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (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 ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv ⋯ hb hc)

The two padded stalk maps agree through the shear (the first half of the kernel argument): at an embedded point y, δ₂ = δ₁ ∘ Ψ^* — ringHom_ext_of_coord' on the constants and on the coordinate germs of the right-padded ambient (padStalkMap_shear_coord, the two lifts' coordinate identities H₁, H₂).

theorem Hironaka.Manifold.stalkIdeal_padIdeal_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₂) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy₁ : E₁.modelPoint y ∈ O₁) (hy₂ : E₂.modelPoint y ∈ O₂) (h₂ : j₂ (E₁.modelPoint y) = E₂.modelPoint y) (H₂ : ∀ (k : Fin m), (E₂.modelStalkMap y) (modelCoordGerm (E₂.modelPoint y) k) = (E₁.modelStalkMap y) (modelGerm (fun (v : Fin n → 𝕜) => j₂ v k) ⋯ hy₁)) (H₁ : ∀ (k : Fin n), (E₁.modelStalkMap y) (modelCoordGerm (E₁.modelPoint y) k) = (E₂.modelStalkMap y) (modelGerm (fun (v : Fin m → 𝕜) => j₁ v k) ⋯ hy₂)) (hb : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source) (hc : ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)) : Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.castAddEmb m) E₁.ideal) (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = Ideal.map (Manifold.germMapOn ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv ⋯ hb hc) (Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.natAddEmb n) E₂.ideal) (padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)))

The kernel argument (the ideals are compared through their restrictions to the piece, never through zero sets): at an embedded point, the stalk of the left-padded ideal is the image under the shear's stalk map of the stalk of the right-padded ideal — both are kernels of padded stalk maps, which the shear interchanges by the coordinate identities of the two lifts.

Off the embedded points, and the ideal identity on the source

theorem Hironaka.Manifold.PieceEmbedding.stalkIdeal_eq_top_of_forall_ne {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} {N : ℕ} (P : PieceEmbedding 𝕜 N X V) (z : (pieceAmbient 𝕜 P.G).carrier) (h : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), P.ambientPoint y ≠ z) : Manifold.IdealSheaf.stalkIdeal P.ideal z = ⊤

Off the embedded points the ideal of a piece embedding has the unit stalk: the embedded points are the cosupport of the ideal, emb being an isomorphism onto the closed subspace.

theorem Hironaka.Manifold.stalkIdeal_padIdeal_eq_top_of_forall_ne {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {N : ℕ} (σ : Fin n ↪ Fin N) (z : (pieceAmbient 𝕜 (padOpens σ E.G)).carrier) (h : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), padExt σ E.G (E.ambientPoint y) ≠ z) : Manifold.IdealSheaf.stalkIdeal (padIdeal σ E.ideal) z = ⊤

The padded form: off the padded embedded points the padded ideal has the unit stalk.

theorem Hironaka.Manifold.padExt_mem_source_of_padExt_mem_target {𝕜 : 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) (y : ↑↑(X.restrictSet V).toPresheafedSpace) (h : padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).target) : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source ∧ ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)

An embedded point of the right padding in the target of the shear is the image of the corresponding embedded point of the left padding, which lies in the source.

theorem Hironaka.Manifold.stalkIdeal_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)) (z : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (hz : z ∈ (shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).source) : Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.castAddEmb m) E₁.ideal) z = Ideal.map (Manifold.germMapOn ↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv ⋯ hz ⋯) (Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.natAddEmb n) E₂.ideal) (↑(shearAmbient E₁ E₂ x O₁ j₂ hj₂ O₂ j₁ hj₁).toPartialEquiv z))

The ideal identity on the source of the shear ([Kol07, Lemma 39]): at every point of the source, the stalk of the left-padded ideal is the image of the stalk of the right-padded ideal under the stalk map of the shear — the kernel argument at the embedded points, ⊤ = ⊤ off them.

The equivalence of two embeddings

theorem Hironaka.Manifold.pullback_padIdeal_inclusion_eq_of_shear {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E₁ : PieceEmbedding 𝕜 n X V) (E₂ : PieceEmbedding 𝕜 m X V) (Ψₐ : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier ⊤) (g : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict { carrier := Ψₐ.source, is_open' := ⋯ }).carrier ((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).restrict { carrier := Ψₐ.target, is_open' := ⋯ }).carrier ⊤) (hg : ∀ (z : ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict { carrier := Ψₐ.source, is_open' := ⋯ }).carrier), ↑(g z) = ↑Ψₐ.toPartialEquiv ↑z) (hideal : ∀ (z : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (hz : z ∈ Ψₐ.source), Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.castAddEmb m) E₁.ideal) z = Ideal.map (Manifold.germMapOn ↑Ψₐ.toPartialEquiv ⋯ hz ⋯) (Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.natAddEmb n) E₂.ideal) (↑Ψₐ.toPartialEquiv z))) : Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).inclusion { carrier := Ψₐ.source, is_open' := ⋯ }) ⋯ (padIdeal (Fin.castAddEmb m) E₁.ideal) = Manifold.IdealSheaf.pullback ⇑↑g ⋯ (Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).inclusion { carrier := Ψₐ.target, is_open' := ⋯ }) ⋯ (padIdeal (Fin.natAddEmb n) E₂.ideal))

The ideal identity on the restrictions for the explicit shear witnesses (the fourth clause of exists_padded_equivalence_of_shear, extracted): the left-padded ideal restricted to the source equals the pullback along g of the right-padded ideal restricted to the target — pointwise through the stalk maps of the inclusions (stalkIdeal_pullback, germMapOn_germMapOn).

theorem Hironaka.Manifold.exists_padded_equivalence_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) (Ψₐ : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier ⊤) (g : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict { carrier := Ψₐ.source, is_open' := ⋯ }).carrier ((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).restrict { carrier := Ψₐ.target, is_open' := ⋯ }).carrier ⊤) (hg : ∀ (z : ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict { carrier := Ψₐ.source, is_open' := ⋯ }).carrier), ↑(g z) = ↑Ψₐ.toPartialEquiv ↑z) (hx : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint x) ∈ Ψₐ.source) (hideal : ∀ (z : (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (hz : z ∈ Ψₐ.source), Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.castAddEmb m) E₁.ideal) z = Ideal.map (Manifold.germMapOn ↑Ψₐ.toPartialEquiv ⋯ hz ⋯) (Manifold.IdealSheaf.stalkIdeal (padIdeal (Fin.natAddEmb n) E₂.ideal) (↑Ψₐ.toPartialEquiv z))) (hpt : ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace), padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ Ψₐ.source → ↑Ψₐ.toPartialEquiv (padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y)) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)) : ∃ (W₁ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) (g : AnalyticMap ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict W₁) ((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).restrict W₂)), padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint x) ∈ W₁ ∧ IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ ⇑g ∧ Function.Bijective ⇑g ∧ Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).inclusion W₁) ⋯ (padIdeal (Fin.castAddEmb m) E₁.ideal) = Manifold.IdealSheaf.pullback ⇑g ⋯ (Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).inclusion W₂) ⋯ (padIdeal (Fin.natAddEmb n) E₂.ideal)) ∧ ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ W₁), ↑(g ⟨padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y), hy⟩) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)

The assembly of the equivalence from a local analytic isomorphism Ψ of the padded ambients that carries the left-padded ambient points to the right-padded ones and the right-padded ideal to the left-padded one: W₁ := Ψ.source, W₂ := Ψ.target, g := Ψ restricted; the ideal identity on the restrictions is the pointwise identity through the stalk maps of the inclusions.

theorem Hironaka.Manifold.embeddings_equivalent_under_automorphism_pad {𝕜 : 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 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).carrier) (W₂ : TopologicalSpace.Opens (pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).carrier) (g : AnalyticMap ((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).restrict W₁) ((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).restrict W₂)), padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint x) ∈ W₁ ∧ IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n + m) → 𝕜)) ⊤ ⇑g ∧ Function.Bijective ⇑g ∧ Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 (padOpens (Fin.castAddEmb m) E₁.G)).inclusion W₁) ⋯ (padIdeal (Fin.castAddEmb m) E₁.ideal) = Manifold.IdealSheaf.pullback ⇑g ⋯ (Manifold.IdealSheaf.pullback ⇑((pieceAmbient 𝕜 (padOpens (Fin.natAddEmb n) E₂.G)).inclusion W₂) ⋯ (padIdeal (Fin.natAddEmb n) E₂.ideal)) ∧ ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y) ∈ W₁), ↑(g ⟨padExt (Fin.castAddEmb m) E₁.G (E₁.ambientPoint y), hy⟩) = padExt (Fin.natAddEmb n) E₂.G (E₂.ambientPoint y)

The equivalence of two embeddings, in padded form ([Kol07, Lemma 39]): the shear Ψ = chart₂⁻¹ ∘ Φ₁⁻¹ ∘ Φ₂ ∘ chart₁ built from the two local lifts, restricted from its source W₁ to its target W₂, carries the left-padded ambient points s₁(i₁(y)) to the right-padded ones s₂(i₂(y)) and pulls the right-padded ideal back to the left-padded one — everything on the padded ambients Sp(padOpens σ G) and with the padded ideals padIdeal σ 𝓘 (the forms of the padded embeddings padLeft/padRight up to unfolding).

theorem Hironaka.Manifold.embeddings_equivalent_under_automorphism {𝕜 : 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 ∧ ((E₁.padLeft m).ambientTriple.pullback ((pieceAmbient 𝕜 (E₁.padLeft m).G).inclusion W₁) ⋯).IsPullbackOf ((E₂.padRight n).ambientTriple.pullback ((pieceAmbient 𝕜 (E₂.padRight n).G).inclusion W₂) ⋯) g ∧ ∀ (y : ↑↑(X.restrictSet V).toPresheafedSpace) (hy : (E₁.padLeft m).ambientPoint y ∈ W₁), ↑(g ⟨(E₁.padLeft m).ambientPoint y, hy⟩) = (E₂.padRight n).ambientPoint y

Two embeddings of one piece are equivalent under a local automorphism of the padded ambient — the analytic form of [Kol07, Lemma 39] (compare [Wlo09, §7.1]), from the padded form through the identifications (E.padLeft m).ambientPoint y = s₁ (i(y)), (E.padRight n).ambientPoint y = s₂ (i(y)) and the empty divisors.