The restricted blow-down off the centre

For a blowing-up π : M' → M along a closed submanifold Y ⊆ S of a closed submanifold S, and the strict transform S' = closure (π⁻¹(S ∖ Y)), the restricted blow-down π|_{S'} : S' → S (IsClosedSubmanifold.restrictMap, between the bundled submanifolds) has the properties of a blowing-up of S along Y in the sense of [BM88, Definition 4.1] away from the exceptional divisor, read off the ambient IsBlowUp. This is the manifold form of Kollár's identification of the stage S_{i+1} := Bl_{Z_i ∩ S_i} S_i of a restricted blow-up sequence with the birational transform of S_i [Kol07, Definition 30.2]:

• it is proper (S' is closed in M'; isProperMap_restrictMap);
• it is a bijection S' ∖ π⁻¹(Y) → S ∖ Y (bijOn_restrictMap_compl: the ambient bijection, and π⁻¹(S ∖ Y) ⊆ S');
• S' ∖ π⁻¹(Y) is dense in S' — by the definition of S' as a closure (dense_preimage_compl_restrictMap);
• it is a local analytic isomorphism there (isLocalDiffeomorphOn_restrictMap_compl): the local inverse Ψ of π at a point of S' off Y restricts to the submanifolds, Ψ⁻¹ carrying S ∩ Ψ.target ∖ Y into π⁻¹(S ∖ Y) ⊆ S' (restrictPartialDiffeomorph), analytic for the induced charts because a map into a closed submanifold is analytic as soon as its composite with the inclusion is (IsClosedSubmanifold.contMDiffAt_of_val, the local form of IsClosedSubmanifold.contMDiff_codRestrict).

The chart clauses of IsBlowUp over the centre are proved in Lift.lean. Not in the sources; the arguments are routine.

Analyticity into a closed submanifold, locally

theorem Manifold.IsClosedSubmanifold.contMDiffAt_of_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {N : Type u} [TopologicalSpace N] [ChartedSpace F N] (hS : IsClosedSubmanifold ψ S s) {g : N → ↑S} {x : N} (hg : ContMDiffAt (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 E) ⊤ (Subtype.val ∘ g) x) : ContMDiffAt (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ g x

A map into a closed submanifold is analytic at a point for the induced charts as soon as its composite with the inclusion is: in the induced chart at the image point it reads projCompl σ ∘ ψ ∘ φ ∘ (val ∘ g) (the local form of IsClosedSubmanifold.contMDiff_codRestrict).

The restricted blow-down off the centre

theorem Manifold.isProperMap_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} (hS : IsClosedSubmanifold ψ S s) (h : IsBlowUp ψ Y c π) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) : IsProperMap ⇑(hS'.restrictMap hS π ⋯ ⋯)

The restricted blow-down is proper: S' is closed in M' and S is Hausdorff.

theorem Manifold.bijOn_restrictMap_compl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} (hS : IsClosedSubmanifold ψ S s) (h : IsBlowUp ψ Y c π) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) : Set.BijOn (⇑(hS'.restrictMap hS π ⋯ ⋯)) (⇑(hS'.restrictMap hS π ⋯ ⋯) ⁻¹' (hS.preimageVal Y)ᶜ) (hS.preimageVal Y)ᶜ

The restricted blow-down is a bijection S' ∖ π⁻¹(Y) → S ∖ Y (the ambient bijection of IsBlowUp, and π⁻¹(S ∖ Y) ⊆ S').

theorem Manifold.dense_preimage_compl_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} (hS : IsClosedSubmanifold ψ S s) (h : IsBlowUp ψ Y c π) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) : Dense (⇑(hS'.restrictMap hS π ⋯ ⋯) ⁻¹' (hS.preimageVal Y)ᶜ)

S' ∖ π⁻¹(Y) is dense in S': S' is the closure of π⁻¹(S ∖ Y).

theorem Manifold.invFun_mem_strictTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {Y : Set M} (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤) (hΨ : Set.EqOn π (↑Ψ.toPartialEquiv) Ψ.source) {y : M} (hy : y ∈ Ψ.target) (hyS : y ∈ S) (hyY : y ∉ Y) : Ψ.invFun y ∈ strictTransformSet π Y S

The local inverse Ψ of π at a point off the centre carries S ∩ Ψ.target ∖ Y into S'.

noncomputable def Manifold.restrictInvFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} (hS : IsClosedSubmanifold ψ S s) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤) (hΨ : Set.EqOn π (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : hS'.toAnalyticManifold.carrier) (y : hS.toAnalyticManifold.carrier) : hS'.toAnalyticManifold.carrier

The inverse of the restricted blow-down near a point off the centre: the local inverse Ψ of π read on S ∩ Ψ.target ∖ Y (junk p₀ elsewhere).

Equations

• Manifold.restrictInvFun hS hS' Ψ hΨ p₀ y = if hy : ↑y ∈ Ψ.target ∧ ↑y ∉ Y then ⟨Ψ.invFun ↑y, ⋯⟩ else p₀

theorem Manifold.restrictInvFun_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} (hS : IsClosedSubmanifold ψ S s) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤) (hΨ : Set.EqOn π (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : hS'.toAnalyticManifold.carrier) {y : hS.toAnalyticManifold.carrier} (hy : ↑y ∈ Ψ.target ∧ ↑y ∉ Y) : restrictInvFun hS hS' Ψ hΨ p₀ y = ⟨Ψ.invFun ↑y, ⋯⟩

noncomputable def Manifold.restrictPartialDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤) (hΨ : Set.EqOn π (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : hS'.toAnalyticManifold.carrier) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) hS'.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤

The local inverse of π at a point of S' off the centre, restricted to the submanifolds: a partial diffeomorphism of the bundled S' and S agreeing with the restricted blow-down on S' ∩ Ψ.source ∖ π⁻¹(Y).

Equations

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

theorem Manifold.isLocalDiffeomorphOn_restrictMap_compl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) s) : IsLocalDiffeomorphOn (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ (⇑(hS'.restrictMap hS π ⋯ ⋯)) (⇑(hS'.restrictMap hS π ⋯ ⋯) ⁻¹' (hS.preimageVal Y)ᶜ)

The restricted blow-down is a local analytic isomorphism off the centre: the restriction of the ambient local inverse to the submanifolds.