The padding tools instantiated

PadIdeal.lean pads an ideal sheaf on a piece ambient along an embedding of coordinates σ : Fin m ↪ Fin n': the padded open, the padded ideal 𝓘 + (z_j)_{j ∉ range σ}, the slice isomorphism of closed subspaces, the transport of reducedness and the nonvanishing of the padded ideal at every stalk for a non-surjective σ (Włodarczyk's common ambient dimension [Wlo09, §7.1]; Kollár's enlargement of the affine space of an embedding [Kol07, Theorem 36, proof]). This module reads those constructions at σ := Fin.castLEEmb h (z ↦ (z, 0)) into the interface PadTools of PieceModel.lean, so that exists_localEmbeddingData_of_padTools yields the existence of local embedding data outright.

noncomputable def Hironaka.Manifold.padTools (𝕜 : Type) [RCLike 𝕜] : PadTools 𝕜

The padding constructions of PadIdeal.lean at σ := Fin.castLEEmb h, as the interface PadTools used by the existence proof of local embedding data ([Wlo09, §7.1]).

Equations

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