The strict transform of a hypersurface in the blow-up charts

The strict transform of H ⊆ M under the blowing-up π with centre Y is H' = closure (π⁻¹(H ∖ Y)) (strictTransformSet; [BM97, §3, "The strict transform"]). Set forms: H' ⊆ π⁻¹(H) for closed H and π⁻¹(H) ⊆ H' ∪ π⁻¹(Y) (strictTransform_subset_preimage, preimage_subset_strictTransform_union). Chart forms, with the adapted chart as hypothesis: for H = {z_k = 0} on an adapted chart φ of Y and a blow-up chart Φ of index i over it (z_{σ k} ∘ π = u_i u_k for k ≠ i, z_{σ i} ∘ π = u_i, w_j ∘ π = w_j off the centre, by IsBlowUpChart.comm and the pointwise formulas for blowUpChartMap), H' ∩ Φ.source = {u_k = 0} for a centre index k ≠ i (strictTransform_inter_source_of_ne), H' ∩ Φ.source = ∅ for k = i (strictTransform_inter_source_self), and H' ∩ Φ.source = {w_j = 0} = π⁻¹(H) ∩ Φ.source for an off-centre index j (strictTransform_inter_source_off, strictTransform_eq_preimage_inter). These are the local computations of the proof of [Kol07, Theorem 88] ("S₁ = (y₁ = 0) is the birational transform of S"; only r − 1 of the r charts meet the strict transform). The inclusions ⊆ read the vanishing of a chart coordinate on π⁻¹(H ∖ Y) (where u_i ≠ 0) through the closure (coord_eq_zero_of_mem_closure); the inclusions ⊇ approximate a point of the coordinate hyperplane by points with u_i ≠ 0, perturbing the scaling coordinate (mem_closure_of_coord_eq_zero).

Codimension-s forms: in flag coordinates Y = {z_σ = 0} ⊆ S = {z_{σ (τ j)} = 0} the strict transform of S misses the blow-up charts of index i ∈ range τ (strictTransform_inter_source_of_mem_range) and is {u_{σ (τ j)} = 0 ∀ j} on the others (strictTransform_inter_source_of_not_mem_range, isAdaptedChart_strictTransform_of_not_mem_range), by the multi-coordinate perturbation mem_closure_of_forall_coord_eq, of which mem_closure_of_coord_eq_zero is the one-coordinate case. These describe the strict transform of a smooth subvariety containing the centre, as in the proof of [Kol07, Theorem 88].

theorem Manifold.strictTransform_subset_preimage {M : Type u} [TopologicalSpace M] {Y : Set M} {M' : Type u} [TopologicalSpace M'] {π : M' → M} {H : Set M} (hπ : Continuous π) (hH : IsClosed H) : strictTransformSet π Y H ⊆ π ⁻¹' H

The strict transform of a closed set lies over it.

theorem Manifold.preimage_subset_strictTransform_union {M : Type u} {Y : Set M} {M' : Type u} [TopologicalSpace M'] {π : M' → M} {H : Set M} : π ⁻¹' H ⊆ strictTransformSet π Y H ∪ π ⁻¹' Y

The preimage of H is covered by the strict transform and the exceptional divisor.

theorem Manifold.mem_closure_of_forall_coord_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {c : ℕ} {M' : Type u} [TopologicalSpace M'] {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} (hp : p ∈ Φ.source) (A : Set M') (hA : ∀ q ∈ Φ.source, (∀ (j : Fin n), j ≠ σ i → ψ (↑Φ q) j = ψ (↑Φ p) j) → ψ (↑Φ q) (σ i) ≠ 0 → q ∈ A) : p ∈ closure A

Multi-coordinate form (for the flag charts of the codimension-s forms): a point of a blow-up chart is a limit of points of the chart with the same coordinates except the scaling coordinate u_{σ i}, which is made nonzero (perturb the scaling coordinate alone); the one-coordinate form is mem_closure_of_coord_eq_zero.

theorem Manifold.mem_closure_of_coord_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {c : ℕ} {M' : Type u} [TopologicalSpace M'] {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {j : Fin n} (hj : j ≠ σ i) {p : M'} (hp : p ∈ Φ.source) (S : Set M') (hS : ∀ q ∈ Φ.source, ψ (↑Φ q) j = ψ (↑Φ p) j → ψ (↑Φ q) (σ i) ≠ 0 → q ∈ S) : p ∈ closure S

A point of a blow-up chart at which a coordinate function other than the scaling coordinate vanishes is a limit of points of the chart at which that coordinate still vanishes and the scaling coordinate does not (perturb the scaling coordinate).

theorem Manifold.continuousOn_coord_fn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M' : Type u} [TopologicalSpace M'] (Φ : OpenPartialHomeomorph M' E) (j : Fin n) : ContinuousOn (fun (q : M') => ψ (↑Φ q) j) Φ.source

The coordinate functions of a chart are continuous on its source.

theorem Manifold.coord_eq_zero_of_mem_closure {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M' : Type u} [TopologicalSpace M'] {Φ : OpenPartialHomeomorph M' E} {A : Set M'} (j : Fin n) (hA : ∀ q ∈ Φ.source ∩ A, ψ (↑Φ q) j = 0) {p : M'} (hp : p ∈ Φ.source) (hpA : p ∈ closure A) : ψ (↑Φ p) j = 0

A coordinate function vanishing on Φ.source ∩ A vanishes on Φ.source ∩ closure A.

theorem Manifold.strictTransform_inter_source_of_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {H : Set M} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {k : Fin c} (hH : ∀ x ∈ φ.source, x ∈ H ↔ ψ (↑φ x) (σ k) = 0) (hik : i ≠ k) : strictTransformSet π Y H ∩ Φ.source = {p : M' | p ∈ Φ.source ∧ ψ (↑Φ p) (σ k) = 0}

For H = {z_k = 0} with k a centre index, the strict transform is {u_k = 0} in the blow-up charts of index i ≠ k.

theorem Manifold.strictTransform_inter_source_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {H : Set M} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hH : ∀ x ∈ φ.source, x ∈ H ↔ ψ (↑φ x) (σ i) = 0) : strictTransformSet π Y H ∩ Φ.source = ∅

For H = {z_k = 0} with k a centre index, the strict transform misses the blow-up chart of index k.

theorem Manifold.strictTransform_inter_source_off {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {H : Set M} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {j : Fin n} (hj : ∀ (k : Fin c), σ k ≠ j) (hH : ∀ x ∈ φ.source, x ∈ H ↔ ψ (↑φ x) j = 0) : strictTransformSet π Y H ∩ Φ.source = {p : M' | p ∈ Φ.source ∧ ψ (↑Φ p) j = 0}

For H = {w_j = 0} with j off the centre (Y transverse to H), the strict transform is {w_j = 0} in every blow-up chart.

theorem Manifold.strictTransform_eq_preimage_inter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {H : Set M} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {j : Fin n} (hj : ∀ (k : Fin c), σ k ≠ j) (hH : ∀ x ∈ φ.source, x ∈ H ↔ ψ (↑φ x) j = 0) : strictTransformSet π Y H ∩ Φ.source = π ⁻¹' H ∩ Φ.source

For H = {w_j = 0} with j off the centre, the strict transform is the total transform on the chart.

Codimension-s forms: flag coordinates

theorem Manifold.IsAdaptedChart.flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {S : Set M} {s : ℕ} {τ : Fin s ↪ Fin c} (hφ : IsAdaptedChart ψ Y φ σ) (hS : ∀ x ∈ φ.source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑φ x) (σ (τ j)) = 0) : IsAdaptedChart ψ S φ (τ.trans σ)

In flag coordinates (Y = {z_σ = 0}, S = {z_{σ (τ j)} = 0}) the adapted chart of Y is adapted to S with the indices τ.trans σ.

theorem Manifold.strictTransform_inter_source_of_mem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {S : Set M} {s : ℕ} {τ : Fin s ↪ Fin c} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hS : ∀ x ∈ φ.source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑φ x) (σ (τ j)) = 0) (hi : i ∈ Set.range ⇑τ) : strictTransformSet π Y S ∩ Φ.source = ∅

In flag coordinates (S = {z_{σ (τ j)} = 0 ∀ j} on the adapted chart), the strict transform of S misses the blow-up charts whose index is one of the S-coordinates: on such a chart the scaling coordinate u_{σ i} = z_{σ i} ∘ π vanishes exactly over the centre, so π⁻¹(S ∖ Y) misses the chart.

theorem Manifold.strictTransform_inter_source_of_not_mem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {S : Set M} {s : ℕ} {τ : Fin s ↪ Fin c} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hS : ∀ x ∈ φ.source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑φ x) (σ (τ j)) = 0) (hi : i ∉ Set.range ⇑τ) : strictTransformSet π Y S ∩ Φ.source = {p : M' | p ∈ Φ.source ∧ ∀ (j : Fin s), ψ (↑Φ p) (σ (τ j)) = 0}

In flag coordinates, the strict transform of S is {u_{σ (τ j)} = 0 ∀ j} on the blow-up charts whose index is not one of the S-coordinates.

theorem Manifold.isAdaptedChart_strictTransform_of_not_mem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {S : Set M} {s : ℕ} {τ : Fin s ↪ Fin c} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) (hS : ∀ x ∈ φ.source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑φ x) (σ (τ j)) = 0) (hi : i ∉ Set.range ⇑τ) : IsAdaptedChart ψ (strictTransformSet π Y S) Φ (τ.trans σ)

On a blow-up chart whose index is not one of the S-coordinates, the chart is adapted to the strict transform of S with the S-indices τ.trans σ.