Padding a local model: the ideal of a piece in more variables

A closed analytic subset Y ⊆ U ⊆ 𝕜ⁿ is also a closed analytic subset of U × 𝕜ᵐ ⊆ 𝕜ⁿ⁺ᵐ, with the equations z_{n+1} = ⋯ = z_{n+m} = 0 added. This is how Włodarczyk brings the local models of an analytic space to a common ambient dimension [Wlo09, §7.1], and how Kollár is free to enlarge the affine space of an embedding, 𝔸ⁿ ↪ 𝔸ⁿ⁺ᵐ, when proving that the resolution does not depend on the embedding [Kol07, Theorem 36, proof]. The construction is used twice: the existence proof of local embedding data (PieceModel.lean) pads local models whose ideal may be zero to a common dimension, and the comparison of two embeddings of a piece pads a piece embedding on either side (PieceEmbedding.padLeft, PieceEmbedding.padRight in PieceIndependence.lean). It is therefore stated for an IDEAL sheaf on a one-piece ambient (pieceAmbient), not for a PieceEmbedding, and indexed by an arbitrary embedding of coordinates σ : Fin n ↪ Fin n' (σ := Fin.castLEEmb keeps the given coordinates as the first n, σ := Fin.natAddEmb as the last n).

For G ⊆ 𝕜ⁿ open, J an ideal sheaf on pieceAmbient 𝕜 G and σ : Fin n ↪ Fin n':

• padOpens σ G := {z ∈ 𝕜ⁿ' | z ∘ σ ∈ G} and padIdeal σ J, the pullback of J along the coordinate projection p : z ↦ z ∘ σ joined with the ideal sheaf 𝓘_S of the coordinate slice S := {z | z_j = 0 for j ∉ range σ} — a closed submanifold of codimension n' − n (isClosedSubmanifold_padSlice; its ideal sheaf is IsClosedSubmanifold.idealSheaf, whose stalks are the germs vanishing on S, spanned by the complementary coordinates).
• The slice isomorphism padSliceHom : Sp(padOpens σ G)/padIdeal σ J ≅ Sp(G)/J (isIso_padSliceHom, padSliceIso): the functoriality of the closed subspace along Sp(p) (p^*J ≤ padIdeal σ J, QuotientSpace.map). It is an isomorphism because the zero extension s : w ↦ (w on range σ, 0 off it) is a section of p with image S: on points, p and s are inverse homeomorphisms between the two supports; on stalks, the fibre map 𝒪_{n,w}/J_w → 𝒪_{n',s(w)}/(p^*J + 𝓘_S)_{s(w)} is bijective since (p^*J + 𝓘_S)_{s(w)} = (s^*)⁻¹ J_w (stalkIdeal_padIdeal_padExt): s^* ∘ p^* = id, s^* kills 𝓘_S, and every germ g at s(w) is congruent to p^*(s^* g) modulo 𝓘_S (the difference vanishes on S). This is the one piece of algebra of the padding; it is done once here.
• isReduced_padIdeal: padIdeal σ J is reduced when J is — its stalks on S are (s^*)⁻¹ of radical ideals, off S the unit ideal.
• isNonzeroEverywhere_padIdeal: for σ not surjective, padIdeal σ J is nonzero at every stalk — a complementary coordinate germ lies in 𝓘_S ⊆ padIdeal σ J and is nonzero (coord_ne_zero); isNonzeroEverywhere_padIdeal_castLE is the Fin.castLEEmb case for n < n'. This is how the padding coordinate supplies PieceEmbedding.isNonzeroEverywhere for a smooth piece with no equations.

Conventions: the one-piece ambient pieceAmbient 𝕜 G (points ⟨(), z⟩); the linear chart of 𝕜ⁿ' is the identity (ContinuousLinearEquiv.refl). Boundary cases: σ surjective (n = n') gives a slice equal to the whole ambient, so that the complement of S is empty — the padded open, the padded ideal, the slice isomorphism and the reducedness hold, the nonvanishing needs ¬ Surjective σ; J = ⊥ (a smooth piece with no equations) is allowed, and the nonvanishing is then the only source of IsNonzeroEverywhere for the padded ideal. Not in the sources beyond the remarks cited; the algebra is elementary.

The padded open, the projection and the zero extension

def Hironaka.Manifold.padOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : TopologicalSpace.Opens (Fin n' → 𝕜)

The padded open {z ∈ 𝕜ⁿ' | z ∘ σ ∈ G}, the preimage of G under the coordinate projection along σ — for σ = Fin.castLEEmb, the U × 𝕜ᵐ of [Wlo09, §7.1].

Equations

• Hironaka.Manifold.padOpens σ G = { carrier := (fun (z : Fin n' → 𝕜) => z ∘ ⇑σ) ⁻¹' ↑G, is_open' := ⋯ }

theorem Hironaka.Manifold.mem_padOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) {z : Fin n' → 𝕜} : z ∈ padOpens σ G ↔ z ∘ ⇑σ ∈ G

def Hironaka.Manifold.padCoordProj {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : (pieceAmbient 𝕜 (padOpens σ G)).carrier → (pieceAmbient 𝕜 G).carrier

The coordinate projection p : z ↦ z ∘ σ on the one-piece ambients.

Equations

• Hironaka.Manifold.padCoordProj σ G x = ⟨x.fst, ⟨↑x.snd ∘ ⇑σ, ⋯⟩⟩

theorem Hironaka.Manifold.padCoordProj_snd {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x : (pieceAmbient 𝕜 (padOpens σ G)).carrier) : ↑(padCoordProj σ G x).snd = ↑x.snd ∘ ⇑σ

theorem Hironaka.Manifold.extend_comp {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (w : Fin n → 𝕜) : Function.extend (⇑σ) w 0 ∘ ⇑σ = w

theorem Hironaka.Manifold.extend_mem_padOpens {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : ↥G) : Function.extend (⇑σ) (↑w) 0 ∈ padOpens σ G

noncomputable def Hironaka.Manifold.padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : (pieceAmbient 𝕜 G).carrier → (pieceAmbient 𝕜 (padOpens σ G)).carrier

The zero extension s : w ↦ (w on range σ, 0 off it), a section of padCoordProj with image the coordinate slice padSlice.

Equations

• Hironaka.Manifold.padExt σ G w = ⟨w.fst, ⟨Function.extend (⇑σ) (↑w.snd) 0, ⋯⟩⟩

theorem Hironaka.Manifold.padExt_snd {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : ↑(padExt σ G w).snd = Function.extend (⇑σ) (↑w.snd) 0

theorem Hironaka.Manifold.padExt_apply_of_notMem_range {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) {j : Fin n'} (hj : j ∉ Set.range ⇑σ) : ↑(padExt σ G w).snd j = 0

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

theorem Hironaka.Manifold.padCoordProj_comp_padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : padCoordProj σ G ∘ padExt σ G = id

The coordinate slice S = {z_j = 0 for j ∉ range σ}

def Hironaka.Manifold.padSlice {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Set (pieceAmbient 𝕜 (padOpens σ G)).carrier

The coordinate slice: the points of the padded ambient whose coordinates off range σ vanish — the image of the zero extension padExt.

Equations

• Hironaka.Manifold.padSlice σ G = {x : (Hironaka.Manifold.pieceAmbient 𝕜 (Hironaka.Manifold.padOpens σ G)).carrier | ∀ j ∉ Set.range ⇑σ, ↑x.snd j = 0}

theorem Hironaka.Manifold.padExt_mem_padSlice {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (w : (pieceAmbient 𝕜 G).carrier) : padExt σ G w ∈ padSlice σ G

theorem Hironaka.Manifold.padExt_padCoordProj_of_mem {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) {x : (pieceAmbient 𝕜 (padOpens σ G)).carrier} (hx : x ∈ padSlice σ G) : padExt σ G (padCoordProj σ G x) = x

theorem Hironaka.Manifold.isClosed_padSlice {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : IsClosed (padSlice σ G)

noncomputable def Hironaka.Manifold.padCompl {n n' : ℕ} (σ : Fin n ↪ Fin n') : Fin (n' - n) ↪ Fin n'

The complementary coordinates Fin (n' - n) ↪ Fin n', enumerating (range σ)ᶜ through complEquiv.

Equations

• Hironaka.Manifold.padCompl σ = { toFun := fun (k : Fin (n' - n)) => ↑((Manifold.complEquiv σ).symm k), inj' := ⋯ }

theorem Hironaka.Manifold.padCompl_notMem_range {n n' : ℕ} (σ : Fin n ↪ Fin n') (k : Fin (n' - n)) : (padCompl σ) k ∉ Set.range ⇑σ

theorem Hironaka.Manifold.forall_padCompl_iff {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {z : Fin n' → 𝕜} : (∀ (k : Fin (n' - n)), z ((padCompl σ) k) = 0) ↔ ∀ j ∉ Set.range ⇑σ, z j = 0

theorem Hironaka.Manifold.chartAt_pieceAmbient_apply {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x y : (pieceAmbient 𝕜 (padOpens σ G)).carrier) : ↑(chartAt (Fin n' → 𝕜) x) y = ↑y.snd

The chart of the padded one-piece ambient at any point is the coordinate inclusion ⟨(), z⟩ ↦ z (the lifted chart of the open padOpens σ G ⊆ 𝕜ⁿ').

theorem Hironaka.Manifold.isAdaptedChart_chartAt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) (x : (pieceAmbient 𝕜 (padOpens σ G)).carrier) : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n' → 𝕜)) (padSlice σ G) (chartAt (Fin n' → 𝕜) x) (padCompl σ)

The chart at any point of the padded ambient is adapted to the slice, with the complementary coordinates as the vanishing ones.

theorem Hironaka.Manifold.isClosedSubmanifold_padSlice {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n' → 𝕜)) (padSlice σ G) (n' - n)

The coordinate slice is a closed submanifold of codimension n' − n of the padded ambient, with the coordinate charts as adapted charts.

Analyticity of the projection and of the zero extension

theorem Hironaka.Manifold.contMDiff_padCoordProj {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n' → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (padCoordProj σ G)

theorem Hironaka.Manifold.contDiff_extend {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') : ContDiff 𝕜 ⊤ fun (w : Fin n → 𝕜) => Function.extend (⇑σ) w 0

theorem Hironaka.Manifold.contMDiff_padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') (G : TopologicalSpace.Opens (Fin n → 𝕜)) : ContMDiff (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n' → 𝕜)) ⊤ (padExt σ G)

The padded ideal

noncomputable def Hironaka.Manifold.padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : (pieceAmbient 𝕜 (padOpens σ G)).IdealSheaf

The padded ideal p^*J + 𝓘_S on padOpens σ G: the pullback of J along the coordinate projection joined with the ideal sheaf of the coordinate slice (the equations z_j = 0, j ∉ range σ) — the ideal of Y ⊆ U × 𝕜ᵐ in [Wlo09, §7.1].

Equations

• Hironaka.Manifold.padIdeal σ J = Manifold.IdealSheaf.pullback (Hironaka.Manifold.padCoordProj σ G) ⋯ J + ⋯.idealSheaf

theorem Hironaka.Manifold.stalkIdeal_padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (x : (pieceAmbient 𝕜 (padOpens σ G)).carrier) : Manifold.IdealSheaf.stalkIdeal (padIdeal σ J) x = Ideal.map (Manifold.germMap (padCoordProj σ G) ⋯ x) (Manifold.IdealSheaf.stalkIdeal J (padCoordProj σ G x)) ⊔ ⋯.idealSheaf.stalkIdeal x

theorem Hironaka.Manifold.pullback_le_padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : Manifold.IdealSheaf.pullback (padCoordProj σ G) ⋯ J ≤ padIdeal σ J

theorem Hironaka.Manifold.mem_padSlice_of_mem_cosupport {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) {x : (pieceAmbient 𝕜 (padOpens σ G)).carrier} (hx : x ∈ Manifold.IdealSheaf.support (padIdeal σ J)) : x ∈ padSlice σ G

theorem Hironaka.Manifold.padCoordProj_mem_cosupport {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) {x : (pieceAmbient 𝕜 (padOpens σ G)).carrier} (hx : x ∈ Manifold.IdealSheaf.support (padIdeal σ J)) : padCoordProj σ G x ∈ Manifold.IdealSheaf.support J

The stalk maps s^*, p^* and the transport along p (s w) = w

noncomputable def Hironaka.Manifold.padCoordProjStalk {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) w →+* AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 (padOpens σ G)) (padExt σ G w)

p^* at s w, read at w through p (s w) = w: 𝒪_{n,w} →+* 𝒪_{n',s w} (germMapOn with a chosen target point).

Equations

• Hironaka.Manifold.padCoordProjStalk σ w = Manifold.germMapOn (Hironaka.Manifold.padCoordProj σ G) ⋯ ⋯ ⋯

noncomputable def Hironaka.Manifold.padTransport {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) w →+* AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) (padCoordProj σ G (padExt σ G w))

The transport 𝒪_{n,w} →+* 𝒪_{n,p (s w)} along p (s w) = w (the stalk map of the identity with the chosen target point).

Equations

• Hironaka.Manifold.padTransport σ w = Manifold.germMapOn (fun (y : (Hironaka.Manifold.pieceAmbient 𝕜 G).carrier) => y) ⋯ ⋯ ⋯

noncomputable def Hironaka.Manifold.padTransport' {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) (padCoordProj σ G (padExt σ G w)) →+* AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) w

The inverse transport 𝒪_{n,p (s w)} →+* 𝒪_{n,w}.

Equations

• Hironaka.Manifold.padTransport' σ w = Manifold.germMapOn (fun (y : (Hironaka.Manifold.pieceAmbient 𝕜 G).carrier) => y) ⋯ ⋯ ⋯

theorem Hironaka.Manifold.padExtStalk_padCoordProjStalk {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) (x : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) w) : (Manifold.germMap (padExt σ G) ⋯ w) ((padCoordProjStalk σ w) x) = x

s^* ∘ p^* = id on stalks (p ∘ s = id).

theorem Hironaka.Manifold.padTransport_padTransport' {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) (x : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) (padCoordProj σ G (padExt σ G w))) : (padTransport σ w) ((padTransport' σ w) x) = x

The two transports are inverse.

theorem Hironaka.Manifold.germMap_padCoordProj_padTransport {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) (x : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 G) w) : (Manifold.germMap (padCoordProj σ G) ⋯ (padExt σ G w)) ((padTransport σ w) x) = (padCoordProjStalk σ w) x

p^* at s w (germMap, landing at p (s w)) composed with the transport is padCoordProjStalk.

theorem Hironaka.Manifold.map_padTransport_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (w : (pieceAmbient 𝕜 G).carrier) : Ideal.map (padTransport σ w) (Manifold.IdealSheaf.stalkIdeal J w) = Manifold.IdealSheaf.stalkIdeal J (padCoordProj σ G (padExt σ G w))

The transport carries J_w onto J_{p (s w)} (the transport of stalk ideals along an equality of points).

theorem Hironaka.Manifold.germMap_padExt_eq_zero_of_mem {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) {x : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 (padOpens σ G)) (padExt σ G w)} (hx : x ∈ ⋯.idealSheaf.stalkIdeal (padExt σ G w)) : (Manifold.germMap (padExt σ G) ⋯ w) x = 0

s^* kills the ideal of the slice: a germ vanishing on S composed with s is zero.

theorem Hironaka.Manifold.sub_padCoordProjStalk_mem {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (w : (pieceAmbient 𝕜 G).carrier) (x : AnalyticManifold.IdealSheaf.stalkRing (pieceAmbient 𝕜 (padOpens σ G)) (padExt σ G w)) : x - (padCoordProjStalk σ w) ((Manifold.germMap (padExt σ G) ⋯ w) x) ∈ ⋯.idealSheaf.stalkIdeal (padExt σ G w)

Every germ at s w is congruent to p^*(s^* g) modulo the ideal of the slice: the difference vanishes on S, where s ∘ p = id.

theorem Hironaka.Manifold.stalkIdeal_padIdeal_padExt {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (w : (pieceAmbient 𝕜 G).carrier) : Manifold.IdealSheaf.stalkIdeal (padIdeal σ J) (padExt σ G w) = Ideal.comap (Manifold.germMap (padExt σ G) ⋯ w) (Manifold.IdealSheaf.stalkIdeal J w)

The stalk of the padded ideal on the slice: (p^*J + 𝓘_S)_{s w} = (s^*)⁻¹ J_w, the one piece of algebra of the padding (Y is also a closed analytic subset of U × 𝕜ᵐ, [Wlo09, §7.1]).

theorem Hironaka.Manifold.padExt_mem_cosupport {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) {w : (pieceAmbient 𝕜 G).carrier} (hw : w ∈ Manifold.IdealSheaf.support J) : padExt σ G w ∈ Manifold.IdealSheaf.support (padIdeal σ J)

Reducedness and nonvanishing

theorem Hironaka.Manifold.isReduced_padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (hJ : J.IsReduced) : (padIdeal σ J).IsReduced

The padded ideal is reduced when J is: on the slice its stalks are (s^*)⁻¹ of the radical ideals J_w, off the slice the unit ideal.

theorem Hironaka.Manifold.exists_notMem_range_of_not_surjective {n n' : ℕ} (σ : Fin n ↪ Fin n') (hσ : ¬Function.Surjective ⇑σ) : ∃ (j : Fin n'), j ∉ Set.range ⇑σ

theorem Hironaka.Manifold.isNonzeroEverywhere_padIdeal {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (hσ : ¬Function.Surjective ⇑σ) : Manifold.IdealSheaf.IsNonzeroEverywhere (padIdeal σ J)

For σ not surjective the padded ideal is nonzero at every stalk: off the slice it is the unit ideal, on the slice it contains a complementary coordinate germ, which is nonzero (coord_ne_zero). The added coordinate of [Wlo09, §7.1] thus makes the ideal of a smooth piece without equations nonzero.

theorem Hironaka.Manifold.isNonzeroEverywhere_padIdeal_castLE {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) {h : n ≤ n'} (hlt : n < n') : Manifold.IdealSheaf.IsNonzeroEverywhere (padIdeal (Fin.castLEEmb h) J)

The nonvanishing for the padding σ := Fin.castLEEmb h with n < n' (the case of PieceEmbedding.padLeft, and of the common dimension n' := max nᵢ + 1 in the existence proof of local embedding data).

The slice isomorphism Sp(padOpens σ G)/padIdeal σ J ≅ Sp(G)/J

theorem Hironaka.Manifold.compat_padCoordProj {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : AnalyticSpace.QuotientSpace.Compat (↑(AnalyticSpace.KLocallyRingedSpace.ofManifoldHom (padCoordProj σ G) ⋯)) (padIdeal σ J) J

Compatibility of the ideals with Sp(p): p^*J ≤ padIdeal σ J (QuotientSpace.Compat).

noncomputable def Hironaka.Manifold.padSliceHom {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : (padIdeal σ J).toAnalyticSpace ⟶ J.toAnalyticSpace

The slice morphism Sp(padOpens σ G)/padIdeal σ J ⟶ Sp(G)/J over the coordinate projection z ↦ z ∘ σ: the functoriality of the closed subspace along Sp(p). It is an isomorphism (isIso_padSliceHom); padSliceIso is the isomorphism. This is the identification of Y with its copy in U × 𝕜ᵐ [Wlo09, §7.1].

Equations

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

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

The slice morphism on points is the coordinate projection.

noncomputable def Hironaka.Manifold.padSliceHomeo {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : ↑(Manifold.IdealSheaf.support (padIdeal σ J)) ≃ₜ ↑(Manifold.IdealSheaf.support J)

The projection and the zero extension are inverse homeomorphisms between the supports of the padded ideal and of J.

Equations

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

theorem Hironaka.Manifold.bijective_fiberMap_padSliceHom {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) (z : ↑(AnalyticSpace.QuotientSpace.support (AnalyticSpace.KLocallyRingedSpace.ofManifold 𝕜 (Fin n' → 𝕜) (pieceAmbient 𝕜 (padOpens σ G)).carrier).toLocallyRingedSpace (padIdeal σ J))) : Function.Bijective ⇑(AnalyticSpace.QuotientSpace.fiberMap (↑(AnalyticSpace.KLocallyRingedSpace.ofManifoldHom (padCoordProj σ G) ⋯)) (padIdeal σ J) J ⋯ z)

The fibre maps of the slice morphism are bijective: at a point s w of the slice, 𝒪_{n,p (s w)}/J → 𝒪_{n',s w}/(p^*J + 𝓘_S) — injective since (p^*J + 𝓘_S)_{s w} = (s^*)⁻¹ J_w and s^* ∘ p^* = id, surjective since every germ is p^*(s^* g) modulo 𝓘_S.

theorem Hironaka.Manifold.isIso_padSliceHom {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : CategoryTheory.IsIso (padSliceHom σ J)

The slice morphism is an isomorphism of analytic 𝕜-spaces: a homeomorphism on points (padSliceHomeo) with bijective fibre maps (bijective_fiberMap_padSliceHom), hence an open immersion onto the whole target (Mathlib's LocallyRingedSpace.IsOpenImmersion.of_stalk_iso, to_iso).

noncomputable def Hironaka.Manifold.padSliceIso {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : (padIdeal σ J).toAnalyticSpace ≅ J.toAnalyticSpace

The slice isomorphism Sp(padOpens σ G)/padIdeal σ J ≅ Sp(G)/J of analytic 𝕜-spaces, over the coordinate projection (hom := padSliceHom).

Equations

• Hironaka.Manifold.padSliceIso σ J = CategoryTheory.asIso (Hironaka.Manifold.padSliceHom σ J)

theorem Hironaka.Manifold.padSliceIso_hom {𝕜 : Type} [RCLike 𝕜] {n n' : ℕ} (σ : Fin n ↪ Fin n') {G : TopologicalSpace.Opens (Fin n → 𝕜)} (J : (pieceAmbient 𝕜 G).IdealSheaf) : (padSliceIso σ J).hom = padSliceHom σ J