The algebra of the paddings and the stalk maps of a piece embedding

Two embeddings of one piece into 𝕜ⁿ and 𝕜ᵐ, padded to x ↦ (x, 0) and y ↦ (0, y) in 𝕜ⁿ⁺ᵐ, are carried into each other by the composite of two shears [Kol07, Lemma 39]. This module provides the bookkeeping that the proof of that equivalence (embeddings_equivalent_under_automorphism, PieceLemma39Shear.lean) uses:

• the paddings in Fin.append form — Function.extend (Fin.castAddEmb m) v 0 = Fin.append v 0, Function.extend (Fin.natAddEmb n) w 0 = Fin.append 0 w — and the shears on appended blocks: shearSnd O j hj (append a b) = append a (b + j a), (shearFst O j hj).symm (append a b) = append (a - j b) b (the two automorphisms of [Kol07, Lemma 39, proof]);
• the ambient points of the padded embeddings: (E.padAlong σ).ambientPoint y = padExt σ E.G (E.ambientPoint y) (the slice isomorphism's inverse on points is the zero extension);
• the stalk map of a piece embedding at an embedded point pieceStalkMap E y : 𝒪_{G, i(y)} →+* 𝒪_{X|V, y} (the stalk map of X|V ≅ Sp(G)/𝓘 → Sp(G) at y) and its transport pieceStalkMapAt E y hq to any point q = i(y); its kernel is the stalk of the ideal (stalkIdeal_eq_ker_pieceStalkMapAt), the kernel of the stalk map of the inclusion of a closed subspace (ker_stalkMap_ι) read through the isomorphism emb. This is the form in which the ideal identity of Lemma 39 is proved: two ideals with the same restriction to the piece are equal, without passing through zero sets.

Not in the sources; bookkeeping.

The paddings in Fin.append form

theorem Hironaka.Manifold.natAdd_notMem_range_castAddEmb {n m : ℕ} (i : Fin m) : Fin.natAdd n i ∉ Set.range ⇑(Fin.castAddEmb m)

theorem Hironaka.Manifold.castAdd_notMem_range_natAddEmb {n m : ℕ} (k : Fin n) : Fin.castAdd m k ∉ Set.range ⇑(Fin.natAddEmb n)

theorem Hironaka.Manifold.extend_castAddEmb {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (v : Fin n → 𝕜) : Function.extend (⇑(Fin.castAddEmb m)) v 0 = Fin.append v 0

The left padding in block form: extend (castAddEmb m) v 0 = (v, 0).

theorem Hironaka.Manifold.extend_natAddEmb {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (w : Fin m → 𝕜) : Function.extend (⇑(Fin.natAddEmb n)) w 0 = Fin.append 0 w

The right padding in block form: extend (natAddEmb n) w 0 = (0, w).

theorem Hironaka.Manifold.append_comp_castAdd {𝕜 : Type} {n m : ℕ} (a : Fin n → 𝕜) (b : Fin m → 𝕜) : Fin.append a b ∘ Fin.castAdd m = a

theorem Hironaka.Manifold.append_comp_natAdd {𝕜 : Type} {n m : ℕ} (a : Fin n → 𝕜) (b : Fin m → 𝕜) : Fin.append a b ∘ Fin.natAdd n = b

theorem Hironaka.Manifold.append_add_append {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (a a' : Fin n → 𝕜) (b b' : Fin m → 𝕜) : Fin.append a b + Fin.append a' b' = Fin.append (a + a') (b + b')

theorem Hironaka.Manifold.append_sub_append {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (a a' : Fin n → 𝕜) (b b' : Fin m → 𝕜) : Fin.append a b - Fin.append a' b' = Fin.append (a - a') (b - b')

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

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

theorem Hironaka.Manifold.shearFst_symm_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).symm.toPartialEquiv (Fin.append a b) = Fin.append (a - j b) b

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

theorem Hironaka.Manifold.mem_source_shearSnd {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O : TopologicalSpace.Opens (Fin n → 𝕜)) (j : (Fin n → 𝕜) → Fin m → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O) (z : Fin (n + m) → 𝕜) : z ∈ (shearSnd O j hj).source ↔ z ∘ Fin.castAdd m ∈ O

theorem Hironaka.Manifold.mem_source_shearFst {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (O : TopologicalSpace.Opens (Fin m → 𝕜)) (j : (Fin m → 𝕜) → Fin n → 𝕜) (hj : ContDiffOn 𝕜 ⊤ j ↑O) (z : Fin (n + m) → 𝕜) : z ∈ (shearFst O j hj).source ↔ z ∘ Fin.natAdd n ∈ O

The ambient points of the padded embeddings

theorem Hironaka.Manifold.padSliceIso_inv_val {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (y : ↑↑J.toAnalyticSpace.toPresheafedSpace) : ↑(↑(padSliceIso σ J).inv y) = padExt σ G ↑y

The inverse of the slice isomorphism, on points, is the zero extension.

theorem Hironaka.Manifold.PieceEmbedding.ambientPoint_padAlong {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {n' : ℕ} (σ : Fin n ↪ Fin n') (y : ↑↑(X.restrictSet V).toPresheafedSpace) : (E.padAlong σ).ambientPoint y = padExt σ E.G (E.ambientPoint y)

The ambient point of the padded embedding is the zero extension of the ambient point.

theorem Hironaka.Manifold.PieceEmbedding.ambientPoint_padLeft_snd {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (m : ℕ) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : ↑((E.padLeft m).ambientPoint y).snd = Fin.append (↑(E.ambientPoint y).snd) 0

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

theorem Hironaka.Manifold.PieceEmbedding.ambientPoint_padRight_snd {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (m : ℕ) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : ↑((E.padRight m).ambientPoint y).snd = Fin.append 0 ↑(E.ambientPoint y).snd

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

The stalk map of a piece embedding at an embedded point, and its kernel

noncomputable def Hironaka.Manifold.PieceEmbedding.pieceStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 E.G) (E.ambientPoint y) →+* ↑((X.restrictSet V).presheaf.stalk y)

The stalk map of a piece embedding at an embedded point 𝒪_{G, i(y)} →+* 𝒪_{X|V, y}: the stalk map at y of the composite X|V ≅ Sp(G)/𝓘 → Sp(G).

Equations

• E.pieceStalkMap y = CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(CategoryTheory.CategoryStruct.comp E.emb E.ideal.toAnalyticSpaceι)) y)

noncomputable def Hironaka.Manifold.PieceEmbedding.pieceStalkMapAt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) {q : (pieceAmbient 𝕜 E.G).carrier} (hq : E.ambientPoint y = q) : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 E.G) q →+* ↑((X.restrictSet V).presheaf.stalk y)

The stalk map of a piece embedding read at any point q = i(y) (transported along the equation, Mathlib's stalkCongr).

Equations

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

theorem Hironaka.Manifold.PieceEmbedding.pieceStalkMapAt_rfl {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : E.pieceStalkMapAt y ⋯ = E.pieceStalkMap y

theorem Hironaka.Manifold.PieceEmbedding.stalkIdeal_eq_ker_pieceStalkMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) : Manifold.IdealSheaf.stalkIdeal E.ideal (E.ambientPoint y) = RingHom.ker (E.pieceStalkMap y)

The stalk of a piece embedding's ideal at an embedded point is the kernel of its stalk map (the kernel of the stalk map of the inclusion of a closed subspace, ker_stalkMap_ι, read through the isomorphism emb): the germs of G vanishing on the piece are exactly those pulled back to 0 on X|V. The device by which two ideals defining the same piece are shown equal in the proof of [Kol07, Lemma 39].

theorem Hironaka.Manifold.PieceEmbedding.stalkIdeal_eq_ker_pieceStalkMapAt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) {q : (pieceAmbient 𝕜 E.G).carrier} (hq : E.ambientPoint y = q) : Manifold.IdealSheaf.stalkIdeal E.ideal q = RingHom.ker (E.pieceStalkMapAt y hq)

theorem Hironaka.Manifold.PieceEmbedding.pieceStalkMapAt_eq_zero_iff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (y : ↑↑(X.restrictSet V).toPresheafedSpace) {q : (pieceAmbient 𝕜 E.G).carrier} (hq : E.ambientPoint y = q) (s : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 E.G) q) : (E.pieceStalkMapAt y hq) s = 0 ↔ s ∈ Manifold.IdealSheaf.stalkIdeal E.ideal q

A germ vanishes under the stalk map of the piece iff it lies in the ideal — the membership form of stalkIdeal_eq_ker_pieceStalkMapAt.