The standard blow-up chart map on the model space

In a blow-up chart (condition (2) of [BM88, Definition 4.1], IsBlowUpChart) the blowing-up reads as the polynomial map π_i = blowUpChartMap σ i of 𝕜ⁿ (x_{σ i} ↦ x_{σ i}, x_{σ k} ↦ x_{σ i} x_{σ k}, the other coordinates fixed), and the exceptional divisor as the coordinate hyperplane {x_{σ i} = 0}. This file sets up that model on the affine space Kn 𝕜 n (the universe-lifted 𝕜ⁿ, an analytic manifold over itself):

• stdBlowUpMap 𝕜 σ i : Kn 𝕜 n → Kn 𝕜 n, analytic (contMDiff_stdBlowUpMap);
• off the hyperplane it is the partial diffeomorphism blowUpChartMapDiffeo, so its germ maps there are bijective (germMap_stdBlowUpMap_bijective);
• stdExceptional 𝕜 σ i, the principal ideal sheaf of the coordinate x_{σ i}, the exceptional ideal sheaf of the model (stalkIdeal_stdExceptional).

The model serves the statement that reduction commutes with the strict transform ([BM97, Remark 3.14]); the model statement over ℂ (Rückert) is Hironaka.Manifold.BlowUp.Transform.Reduced.ModelComplex.

noncomputable def Manifold.stdBlowUpMap (𝕜 : Type) [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : AnalyticSpace.Kn 𝕜 n → AnalyticSpace.Kn 𝕜 n

The standard blow-up chart map π_i on the model Kn 𝕜 n.

Equations

• Manifold.stdBlowUpMap 𝕜 σ i x = { down := Manifold.blowUpChartMap σ i x.down }

@[simp]

theorem Manifold.stdBlowUpMap_down {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (x : AnalyticSpace.Kn 𝕜 n) : (stdBlowUpMap 𝕜 σ i x).down = blowUpChartMap σ i x.down

The model map in coordinates.

theorem Manifold.stdBlowUpMap_eq_diffeo {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (x : AnalyticSpace.Kn 𝕜 n) : stdBlowUpMap 𝕜 σ i x = ↑(BlowUpGlue.blowUpChartMapDiffeo (AnalyticSpace.knCoord 𝕜 n) σ i).toPartialEquiv x

The model map is the chart diffeomorphism blowUpChartMapDiffeo read on Kⁿ.

theorem Manifold.contMDiff_stdBlowUpMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : ContMDiff (modelWithCornersSelf 𝕜 (AnalyticSpace.Kn 𝕜 n)) (modelWithCornersSelf 𝕜 (AnalyticSpace.Kn 𝕜 n)) ⊤ (stdBlowUpMap 𝕜 σ i)

The model map is analytic (polynomial).

theorem Manifold.stdBlowUpMap_down_scaling {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (x : AnalyticSpace.Kn 𝕜 n) : (stdBlowUpMap 𝕜 σ i x).down (σ i) = x.down (σ i)

The scaling coordinate is preserved by the model map.

theorem Manifold.germMap_stdBlowUpMap_bijective {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) {q : AnalyticSpace.Kn 𝕜 n} (hq : q.down (σ i) ≠ 0) : Function.Bijective ⇑(germMap (stdBlowUpMap 𝕜 σ i) ⋯ q)

Off the exceptional hyperplane {x_{σ i} = 0} the germ maps of the model map are bijective (it is the partial diffeomorphism blowUpChartMapDiffeo there).

The exceptional ideal sheaf of the model

theorem Manifold.hasLocalGenerators_span_germ_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (t : ↑((structureSheaf 𝕜 E N).presheaf.obj (Opposite.op ⊤))) : IdealSheaf.HasLocalGenerators fun (x : ↑↧N) => Ideal.span {(CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E N).presheaf.germ ⊤ x trivial)) t}

A single global section generates an ideal sheaf (its principal ideal sheaf).

noncomputable def Manifold.stdExceptional (𝕜 : Type) [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : IdealSheaf (structureSheaf 𝕜 (AnalyticSpace.Kn 𝕜 n) (AnalyticSpace.Kn 𝕜 n))

The exceptional ideal sheaf of the model, the principal ideal sheaf of the scaling coordinate x_{σ i}.

Equations

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

theorem Manifold.stalkIdeal_stdExceptional {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (x : AnalyticSpace.Kn 𝕜 n) : (stdExceptional 𝕜 σ i).stalkIdeal x = Ideal.span {(CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 (AnalyticSpace.Kn 𝕜 n) (AnalyticSpace.Kn 𝕜 n)).presheaf.germ ⊤ x trivial)) (AnalyticSpace.coordSection 𝕜 n (σ i))}

The stalks of the model's exceptional ideal sheaf are the principal ideals of the coordinate germ x_{σ i}.

theorem Manifold.mem_cosupport_stdExceptional {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) (x : AnalyticSpace.Kn 𝕜 n) : x ∈ (stdExceptional 𝕜 σ i).support ↔ x.down (σ i) = 0

The cosupport of the model's exceptional ideal sheaf is the coordinate hyperplane {x_{σ i} = 0}.