The blowing-up exists

For Y ⊆ M a closed analytic submanifold of codimension c there is a blowing-up π : M' → M with centre Y: a Hausdorff second-countable analytic manifold M' (in the universe of M) with a proper analytic map π satisfying conditions (1) and (2) of [BM88, Definition 4.1] (exists_isBlowUp). There are three cases.

• 1 ≤ c ≤ n: the glued space of Hironaka.Manifold.BlowUp.Glued with its blow-down, which is a blowing-up by Hironaka.Manifold.BlowUp.GluedCharts, GluedBlowDown, GluedOffCenter and GluedTopology.
• c = 0, a boundary case not considered in the source: Y is open and closed and IsBlowUp ψ Y 0 π forces π⁻¹(Y) = ∅; the blowing-up is the inclusion M ∖ Y → M.
• c > n: there is no block embedding Fin c ↪ Fin n, Y is empty, and the blowing-up is the identity of M.

The type BlowUpSpace ψ hY, its instances and the map blowUpMap ψ hY are a choice of these data; every property of the chosen blowing-up is read off isBlowUp_blowUpMap. This chosen blowing-up is the one from which the sequences of blowings-up of the analytic strand are built.

The inclusion of an open subset as a local diffeomorphism

noncomputable def Manifold.opensValDiffeo {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) (x₀ : ↥U) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (↥U) M ⊤

The inclusion of an open subset, as a partial diffeomorphism onto the subset.

Equations

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

The three cases

theorem Manifold.exists_isBlowUp_of_embedding {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) : ∃ (M' : Type u) (x : TopologicalSpace M') (x_1 : ChartedSpace E M') (x_2 : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M') (x_3 : T2Space M') (x_4 : SecondCountableTopology M') (π : M' → M), IsBlowUp ψ Y c π

The main case 1 ≤ c ≤ n: the glued space with its blow-down is a blowing-up. The witness (σ₀, i₀) is immaterial: it only serves to produce adapted charts at the points off Y (exists_isAdaptedChart_of_notMem), so that the pieces cover M; the glued space, its blow-down and the conclusion do not depend on it.

theorem Manifold.exists_isBlowUp_of_c_eq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} (hY : IsClosedSubmanifold ψ Y 0) : ∃ (M' : Type u) (x : TopologicalSpace M') (x_1 : ChartedSpace E M') (x_2 : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M') (x_3 : T2Space M') (x_4 : SecondCountableTopology M') (π : M' → M), IsBlowUp ψ Y 0 π

The case c = 0: Y is open and closed, and the inclusion M ∖ Y → M is a blowing-up.

theorem Manifold.exists_isBlowUp_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hemp : IsEmpty (Fin c ↪ Fin n)) : ∃ (M' : Type u) (x : TopologicalSpace M') (x_1 : ChartedSpace E M') (x_2 : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M') (x_3 : T2Space M') (x_4 : SecondCountableTopology M') (π : M' → M), IsBlowUp ψ Y c π

The case c > n: no block embedding exists, Y is empty, and the identity is a blowing-up.

theorem Manifold.exists_isBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : ∃ (M' : Type u) (x : TopologicalSpace M') (x_1 : ChartedSpace E M') (x_2 : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M') (x_3 : T2Space M') (x_4 : SecondCountableTopology M') (π : M' → M), IsBlowUp ψ Y c π

The blowing-up exists [BM88, Definition 4.1]: for Y a closed submanifold of codimension c there is a Hausdorff second-countable analytic manifold M' in the universe of M with a proper analytic map π : M' → M satisfying conditions (1) and (2) of the definition.

A chosen blowing-up

def Manifold.BlowUpSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : Type u

The blowing-up of M with centre Y [BM88, Definition 4.1]: a choice of the data of exists_isBlowUp. Its properties are read off isBlowUp_blowUpMap.

Equations

• Manifold.BlowUpSpace ψ hY = ⋯.choose

@[instance_reducible]

noncomputable instance Manifold.instTopologicalSpaceBlowUpSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : TopologicalSpace (BlowUpSpace ψ hY)

The topology of the chosen blowing-up, from exists_isBlowUp.

Equations

• Manifold.instTopologicalSpaceBlowUpSpace ψ hY = ⋯.choose

@[instance_reducible]

noncomputable instance Manifold.instChartedSpaceBlowUpSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : ChartedSpace E (BlowUpSpace ψ hY)

The charts of the chosen blowing-up, from exists_isBlowUp.

Equations

• Manifold.instChartedSpaceBlowUpSpace ψ hY = ⋯.choose

theorem Manifold.blowUpSpace_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : ∃ (x : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ (BlowUpSpace ψ hY)) (x_1 : T2Space (BlowUpSpace ψ hY)) (x_2 : SecondCountableTopology (BlowUpSpace ψ hY)) (π : BlowUpSpace ψ hY → M), IsBlowUp ψ Y c π

The remaining data of the chosen blowing-up.

instance Manifold.instIsManifoldModelWithCornersSelfTopWithTopENatBlowUpSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ (BlowUpSpace ψ hY)

The chosen blowing-up is an analytic manifold.

instance Manifold.instT2SpaceBlowUpSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : T2Space (BlowUpSpace ψ hY)

The chosen blowing-up is Hausdorff.

instance Manifold.instSecondCountableTopologyBlowUpSpace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : SecondCountableTopology (BlowUpSpace ψ hY)

The chosen blowing-up is second countable.

noncomputable def Manifold.blowUpMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : BlowUpSpace ψ hY → M

The blow-down π : M' → M of the chosen blowing-up.

Equations

• Manifold.blowUpMap ψ hY = ⋯.choose

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

The chosen blowing-up is a blowing-up in the sense of [BM88, Definition 4.1].