The model statement over ℂ: the saturation of a reduced pull-back is radical

On the model Kn 𝕜 n of Hironaka.Manifold.BlowUp.Transform.Reduced.StdModel: for an open V and an ideal sheaf I on V with radical stalks, the pull-back π_i^* I along the standard blow-up chart map π_i : π_i⁻¹(V) → V has radical saturation ⋃_k (π_i^* I : x_{σ i}^k) at every point. Over ℂ this is the Rückert core mem_iSup_colon_pow_of_pow_mem of Hironaka.Manifold.BlowUp.Transform.StrictSubspaceReduced (Rückert's Nullstellensatz through the colon sheaf) applied on the open submanifold π_i⁻¹(V): the pull-back is radical off the hyperplane {x_{σ i} = 0} because π_i is a local diffeomorphism there (germMap_stdBlowUpMap_bijective) and I is radical. This is the case over ℂ of [BM97, Remark 3.14] on the model.

A general tool is proved along the way: the germ map of a composite is the composite of the germ maps (germMap_germMap).

theorem Manifold.germMap_germMap {𝕜 : 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} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] {P : Type u} [TopologicalSpace P] [ChartedSpace E'' P] {φ : N → M} (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) {ψ : P → N} (hψ : ContMDiff (modelWithCornersSelf 𝕜 E'') (modelWithCornersSelf 𝕜 E') ⊤ ψ) (b : P) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (φ (ψ b)))) : (germMap ψ hψ b) ((germMap φ hφ (ψ b)) s) = (germMap (φ ∘ ψ) ⋯ b) s

The germ map of a composite is the composite of the germ maps (germMap).

theorem Ideal.IsRadical.map_of_bijective {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Bijective ⇑f) {J : Ideal R} (hJ : J.IsRadical) : (map f J).IsRadical

The image of a radical ideal under a bijective ring homomorphism is radical.

The model map restricted over an open V

@[reducible, inline]

noncomputable abbrev Manifold.stdPreimage (𝕜 : Type) [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)

The open π_i⁻¹(V) of the model.

Equations

• Manifold.stdPreimage 𝕜 σ i V = Manifold.preimageOpens (Manifold.stdBlowUpMap 𝕜 σ i) ⋯ V

noncomputable def Manifold.stdBlowUpMapRestrict (𝕜 : Type) [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : ↥(stdPreimage 𝕜 σ i V) → ↥V

The standard blow-up chart map restricted to π_i⁻¹(V) → V.

Equations

• Manifold.stdBlowUpMapRestrict 𝕜 σ i V x = ⟨Manifold.stdBlowUpMap 𝕜 σ i ↑x, ⋯⟩

@[simp]

theorem Manifold.val_stdBlowUpMapRestrict {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) (x : ↥(stdPreimage 𝕜 σ i V)) : ↑(stdBlowUpMapRestrict 𝕜 σ i V x) = stdBlowUpMap 𝕜 σ i ↑x

The restricted map, as a map of the ambient space.

theorem Manifold.contMDiff_stdBlowUpMapRestrict {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : ContMDiff (modelWithCornersSelf 𝕜 (AnalyticSpace.Kn 𝕜 n)) (modelWithCornersSelf 𝕜 (AnalyticSpace.Kn 𝕜 n)) ⊤ (stdBlowUpMapRestrict 𝕜 σ i V)

The restricted map is analytic.

theorem Manifold.germMap_stdBlowUpMapRestrict_bijective {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) {x : ↥(stdPreimage 𝕜 σ i V)} (hx : (↑x).down (σ i) ≠ 0) : Function.Bijective ⇑(germMap (stdBlowUpMapRestrict 𝕜 σ i V) ⋯ x)

Off the hyperplane {x_{σ i} = 0} the germ maps of the restricted model map are bijective (the square with the two open inclusions and germMap_stdBlowUpMap_bijective).

@[reducible, inline]

noncomputable abbrev Manifold.stdExceptionalRestrict {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) : IdealSheaf (structureSheaf 𝕜 (AnalyticSpace.Kn 𝕜 n) ↥(stdPreimage 𝕜 σ i V))

The exceptional ideal sheaf of the model restricted to π_i⁻¹(V).

Equations

• Manifold.stdExceptionalRestrict σ i V = Manifold.IdealSheaf.pullback Subtype.val ⋯ (Manifold.stdExceptional 𝕜 σ i)

theorem Manifold.mem_cosupport_stdExceptionalRestrict {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) (x : ↥(stdPreimage 𝕜 σ i V)) : x ∈ (stdExceptionalRestrict σ i V).support ↔ (↑x).down (σ i) = 0

The cosupport of the restricted exceptional ideal sheaf is the hyperplane {x_{σ i} = 0}.

theorem Manifold.isRadical_stalkIdeal_pullback_stdBlowUpMapRestrict {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn 𝕜 n)) (I : IdealSheaf (structureSheaf 𝕜 (AnalyticSpace.Kn 𝕜 n) ↥V)) (hI : ∀ (x : ↑↧↥V), (I.stalkIdeal x).IsRadical) {x : ↥(stdPreimage 𝕜 σ i V)} (hx : x ∉ (stdExceptionalRestrict σ i V).support) : ((IdealSheaf.pullback (stdBlowUpMapRestrict 𝕜 σ i V) ⋯ I).stalkIdeal x).IsRadical

The pull-back of a reduced ideal sheaf is radical off the hyperplane (there π_i is a local diffeomorphism).

The model statement over ℂ

theorem Manifold.isRadical_iSup_colon_pullback_complex {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (V : TopologicalSpace.Opens (AnalyticSpace.Kn ℂ n)) (I : IdealSheaf (structureSheaf ℂ (AnalyticSpace.Kn ℂ n) ↥V)) (hI : ∀ (x : ↑↧↥V), (I.stalkIdeal x).IsRadical) (u : ↥(stdPreimage ℂ σ i V)) : (⨆ (k : ℕ), Submodule.colon ((IdealSheaf.pullback (stdBlowUpMapRestrict ℂ σ i V) ⋯ I).stalkIdeal u) ↑((stdExceptionalRestrict σ i V).stalkIdeal u ^ k)).IsRadical

On the model, the saturation of the pull-back of a reduced ideal sheaf along the standard blow-up chart map is radical at every point of π_i⁻¹(V).