Proper simple normal crossings with a submanifold, and its transport by a blowing-up

Kollár restricts a smooth blow-up sequence Π with centres Z_i ⊆ S_i to the strict transforms S_i of a closed submanifold S [Kol07, 30.2], and the blow-up sequences of his algorithm have centres with simple normal crossings with the boundary [Kol07, Definition 66]. For Π|_S to be such a sequence on S the boundary E_i ∩ S_i must have only normal crossings with Z_i ∩ S_i. The invariant carried along Π is the proper form of "S_i has simple normal crossings with E_i" (HypersurfaceFamily.HasSncWithProper): at every point of S_i one chart adapted to S_i which is an snc chart of the family E_i and in which no component's coordinate is an S_i-coordinate — no component contains S_i near the point. (Without "proper" a component could contain S_i, and its trace on S_i would be all of S_i, not a hypersurface; the proper form removes this degenerate case at the root, and the invariant is propagated directly, see hasSncWithProper_totalTransform.)

The transport by one blowing-up π : M' → M along Z ⊆ H (hasSncWithProper_totalTransform): over a point a ∈ Z, the simultaneous chart of Hironaka/Manifold/Snc/FlagProtected.lean (exists_isSncChartAt_flag_proper: adapted to Z, H cut out by the centre block σ ∘ τ, snc for E with component coordinates off that block) lifts to blow-up charts; a blow-up chart of an index k ∈ range τ misses the strict transform of H (strictTransform_inter_source_eq_empty_of_subset, the one-directional form of strictTransform_inter_source_self; Kollár: only r − 1 of the r charts meet the strict transform, [Kol07, Theorem 88, proof]), so a point of H' over a lies in a chart of index k ∉ range τ, where isAdaptedChart_strictTransform_of_not_mem_range adapts the chart to H' with the block τ.trans σ and totalTransform_isSncChartAt keeps the component coordinates (cidx j, off the block) and gives the exceptional divisor σ k, off the block as k ∉ range τ. Off the centre π is a local isomorphism and the proper chart at π p transports along a local inverse (IsBlowUp.exists_transportChart_of_notMem, through transportChart), where the strict transform of H is the preimage of H and the strict transforms of the components are the preimages of the components.

The traces of the boundary on S and the transported invariant are in Hironaka/Manifold/Snc/Trace.lean; the invariant is carried along the restricted sequences of the embedded resolution (Hironaka/Resolution/Analytic/Wlo09/ProperSnc.lean).

def Manifold.HypersurfaceFamily.HasSncWithProper {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : HypersurfaceFamily M) (Y : Set M) (s : ℕ) : Prop

Y has simple normal crossings with F, properly: at every point of Y there is a chart adapted to Y which is an snc chart of F there and in which no component's coordinate is a Y-coordinate — no component of F contains Y near the point. The form of [Kol07, Definition 24 (4)] needed to restrict a blow-up sequence to Y [Kol07, 30.2]; compare HasSncWith, which allows components containing Y.

Equations

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

theorem Manifold.HypersurfaceFamily.HasSncWithProper.hasSncWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {Y : Set M} {s : ℕ} (h : HasSncWithProper ψ F Y s) : HasSncWith ψ F Y s

The proper form implies HasSncWith.

theorem Manifold.HypersurfaceFamily.hasSncWithProper_empty {𝕜 : 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} {s : ℕ} (hY : IsClosedSubmanifold ψ Y s) : HasSncWithProper ψ (empty M) Y s

The empty family has simple normal crossings with every closed submanifold, properly (every adapted chart is an snc chart of the empty family).

Blow-up charts of a flag index miss the strict transform

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

If H ∩ φ.source ⊆ {z_{σ i} = 0} for a centre index i, the strict transform of H misses the blow-up chart of index i (the one-directional form of strictTransform_inter_source_self; Kollár's "only r − 1 of these" charts, [Kol07, Theorem 88, proof]).

theorem Manifold.mem_strictTransformSet_iff_of_notMem {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} {Y H : Set M} (hπ : Continuous π) (hH : IsClosed H) {p : M'} (hpY : π p ∉ Y) : p ∈ strictTransformSet π Y H ↔ π p ∈ H

Off the centre the strict transform of a closed set is its preimage.

Transport of a chart along a local inverse of the blowing-up, off the centre

theorem Manifold.IsBlowUp.exists_transportChart_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} {c : ℕ} {φ : OpenPartialHomeomorph M E} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (hY : IsClosed Y) (h : IsBlowUp ψ Y c π) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {p : M'} (hpY : π p ∉ Y) (hpφ : π p ∈ φ.source) : ∃ e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M', p ∈ e.source ∧ ∀ x ∈ e.source, π x ∉ Y ∧ π x ∈ φ.source ∧ ↑e x = ↑φ (π x)

Off the centre, a chart φ of M at π p transports to a chart e of M' at p whose source lies over φ.source ∖ Y and on which e = φ ∘ π (transportChart along a local inverse of the blowing-up, an analytic isomorphism off the centre, [BM88, Definition 4.1 (1)]).

Transport of the proper invariant by one blowing-up

theorem Manifold.HypersurfaceFamily.hasSncWithProper_totalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {H : Set M} {c : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {F : HypersurfaceFamily M} {Z : Set M} {s : ℕ} (hZ : IsClosedSubmanifold ψ Z c) (h : IsBlowUp ψ Z c π) (hF : IsSnc ψ F) (hH : IsClosedSubmanifold ψ H s) (hZH : Z ⊆ H) (hFZ : HasSncWith ψ F Z c) (hFH : HasSncWithProper ψ F H s) : HasSncWithProper ψ (totalTransform π Z F) (strictTransformSet π Z H) s

The proper invariant is transported by a blowing-up ([Kol07, 30.2] with [Kol07, Definition 25] and the proof of [Kol07, Theorem 88]). Let π : M' → M blow up Z ⊆ H, with F snc, Z having snc with F and H having snc with F properly. Then the strict transform H' of H has snc with the total transform of F, properly. Over a ∈ Z, the simultaneous chart (exists_isSncChartAt_flag_proper) has H cut out by the block σ ∘ τ; a point of H' over a lies in a blow-up chart of an index k ∉ range τ (the charts of the indices τ j miss H', strictTransform_inter_source_eq_empty_of_subset), which is adapted to H' with the block τ.trans σ and an snc chart of the total transform with the component coordinates cidx j ∉ range (τ.trans σ) and the exceptional coordinate σ k, k ∉ range τ. Off the centre the proper chart at π p transports along a local inverse of π (IsBlowUp.exists_transportChart_of_notMem), H' and the strict transforms of the components being the preimages of H and of the components there.