The exceptional divisor and the degenerate centres

For any blowing-up π : M' → M with centre Y in the sense of IsBlowUp [BM88, Definition 4.1]:

• The exceptional divisor. In a blow-up chart of index i the exceptional divisor F = π⁻¹(Y) is the hyperplane {u_i = 0} (IsBlowUpChart.mem_preimage_iff), so F is a closed submanifold of codimension one (IsBlowUp.isClosedSubmanifold_preimage; the exceptional divisor of a smooth blow-up is smooth, [Kol07, Notation 19]). The pullback of the ideal sheaf of Y is the ideal sheaf of F: its stalk at a point of a blow-up chart is generated by the germ of u_i (since z_i ∘ π = u_i and z_j ∘ π = u_i u_j; IsBlowUp.stalkIdeal_pullback_eq_span_coord), and this is the ideal of F in every adapted chart of F, because the kernel of the restriction of germs to F is generated by the adapted coordinate (IsClosedSubmanifold.ker_restrictStalk); hence IsBlowUp.isIdealSheafOf_pullback.
• The degenerate centres. For a centre of codimension one, or an empty centre, the blowing-up is a diffeomorphism (the trivial and the empty blow-up of [Kol07, Warning 20]): it is a bijective local diffeomorphism (IsLocalDiffeomorph.toDiffeomorphOfBijective). For c = 1 the single chart map π_0 is the identity, π reads φ⁻¹ ∘ Φ in a blow-up chart, and two blow-up charts over one adapted chart have inverses agreeing off the hyperplane, hence everywhere by density.

These results enter the uniqueness of the blowing-up (Hironaka.Manifold.BlowUp.Unique) and the transforms of ideal sheaves under it.

def Manifold.singleEmb {n : ℕ} (j : Fin n) : Fin 1 ↪ Fin n

The block embedding Fin 1 ↪ Fin n with value j.

Equations

• Manifold.singleEmb j = { toFun := fun (x : Fin 1) => j, inj' := ⋯ }

@[simp]

theorem Manifold.singleEmb_apply {n : ℕ} (j : Fin n) (k : Fin 1) : (singleEmb j) k = j

The one-element embedding Fin 1 ↪ Fin n picks the index j.

theorem Manifold.blowUpChartMap_fin_one {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (σ : Fin 1 ↪ Fin n) (i : Fin 1) : blowUpChartMap σ i = id

For c = 1 the single chart map is the identity.

Blow-up charts for c = 1

theorem Manifold.IsBlowUpChart.target_eq_of_fin_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} {i : Fin 1} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) : Φ.target = φ.target

For c = 1 a blow-up chart has the target of the adapted chart.

theorem Manifold.IsBlowUpChart.apply_eq_of_fin_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} {i : Fin 1} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) : ↑φ (π p) = ↑Φ p

For c = 1, φ ∘ π = Φ on the source of a blow-up chart.

theorem Manifold.IsBlowUpChart.symm_apply_eq_of_fin_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} {i : Fin 1} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) : ↑φ.symm (↑Φ p) = π p

For c = 1, π = φ⁻¹ ∘ Φ on the source of a blow-up chart.

The exceptional divisor

theorem Manifold.IsBlowUpChart.mem_preimage_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) : p ∈ π ⁻¹' Y ↔ ψ (↑Φ p) (σ i) = 0

In a blow-up chart of index i the exceptional divisor F = π⁻¹(Y) is the hyperplane {u_i = 0}.

theorem Manifold.IsBlowUpChart.isAdaptedChart_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) : IsAdaptedChart ψ (π ⁻¹' Y) Φ (singleEmb (σ i))

A blow-up chart of index i is adapted to the exceptional divisor, with the single block coordinate u_i.

theorem Manifold.IsBlowUpChart.germMap_coord_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} (hπ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) : (germMap π hπ p) (coord E ψ φ hφ ⋯ (σ i)) = coord E ψ Φ ⋯ hp (σ i)

z_i ∘ π = u_i: the pullback of the scaling coordinate of the adapted chart is the scaling coordinate of the blow-up chart.

theorem Manifold.IsBlowUpChart.germMap_coord_of_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} (hπ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) {k : Fin c} (hk : k ≠ i) : (germMap π hπ p) (coord E ψ φ hφ ⋯ (σ k)) = coord E ψ Φ ⋯ hp (σ i) * coord E ψ Φ ⋯ hp (σ k)

z_k ∘ π = u_i u_k for k ≠ i: the pullback of a ratio coordinate.

theorem Manifold.IsBlowUp.isClosedSubmanifold_preimage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) : IsClosedSubmanifold ψ (π ⁻¹' Y) 1

The exceptional divisor is a closed submanifold of codimension one (the exceptional divisor of a smooth blow-up is smooth, [Kol07, Notation 19]).

theorem Manifold.IsBlowUp.stalkIdeal_pullback_eq_span_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (h : IsBlowUp ψ Y c π) {J : IdealSheaf (structureSheaf 𝕜 E M)} (hJ : IsIdealSheafOf ψ Y c J) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) : (IdealSheaf.pullback π ⋯ J).stalkIdeal p = Ideal.span {coord E ψ Φ ⋯ hp (σ i)}

The pullback π^* I_Y · 𝒪_{M'} of the ideal sheaf of the centre is locally principal: in a blow-up chart of index i its stalk is generated by the germ of the coordinate u_i.

theorem Manifold.IsBlowUp.isIdealSheafOf_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {J : IdealSheaf (structureSheaf 𝕜 E M)} (hJ : IsIdealSheafOf ψ Y c J) : IsIdealSheafOf ψ (π ⁻¹' Y) 1 (IdealSheaf.pullback π ⋯ J)

The pullback of the ideal sheaf of Y is the ideal sheaf of the exceptional divisor.

The degenerate centres

def Manifold.IsBlowUpChart.partialDiffeomorphOfFinOne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} {i : Fin 1} {Φ : OpenPartialHomeomorph M' E} (hπ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hΦ : IsBlowUpChart ψ π φ σ i Φ) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤

For c = 1 the blow-down restricted to a blow-up chart, as a partial diffeomorphism onto the source of the adapted chart (inverse Φ⁻¹ ∘ φ).

Equations

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

theorem Manifold.IsBlowUpChart.symm_eqOn_of_fin_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} {i : Fin 1} {Φ : OpenPartialHomeomorph M' E} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (h : IsBlowUp ψ Y 1 π) (hφ : IsAdaptedChart ψ Y φ σ) {Φ' : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hΦ' : IsBlowUpChart ψ π φ σ i Φ') : Set.EqOn (↑Φ.symm) (↑Φ'.symm) φ.target

For c = 1 two blow-up charts over one adapted chart have the same inverse: the inverses agree off the hyperplane (there π is injective) and are continuous, and the hyperplane's complement is dense.

theorem Manifold.IsBlowUp.exists_diffeomorph_of_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (h : IsBlowUp ψ ∅ c π) : ∃ (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤), ∀ (p : M'), g p = π p

For an empty centre the blowing-up is a diffeomorphism (the empty blow-up of [Kol07, Warning 20]).

theorem Manifold.IsBlowUp.exists_diffeomorph_of_codim_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (hY : IsClosedSubmanifold ψ Y 1) (h : IsBlowUp ψ Y 1 π) : ∃ (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤), ∀ (p : M'), g p = π p

For a centre of codimension one the blowing-up is a diffeomorphism (the trivial blow-up of [Kol07, Warning 20]).