The blow-down off the exceptional divisor

Off the exceptional divisor the blow-down of the glued space is an analytic isomorphism onto M ∖ Y, condition (1) of [BM88, Definition 4.1]: in a piece it reads φ⁻¹ ∘ ψ⁻¹ ∘ π_i ∘ ψ, and π_i is a diffeomorphism of {u_i ≠ 0} onto {x_i ≠ 0} with inverse blowUpChartInv, so the blow-down is a local diffeomorphism at every point off the divisor. It is bijective from the complement of the divisor onto M ∖ Y: surjective since every point of M lies under some piece, injective since two points over the same point of M ∖ Y are related by the transition map (uniqueness of the lift off the centre) and π_{i'} is injective on {u_{i'} ≠ 0}.

This is one of the clauses showing that the glued space is a blowing-up (Hironaka.Manifold.BlowUp.Exists).

noncomputable def Manifold.BlowUpGlue.blowUpChartMapDiffeo {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) E E ⊤

The chart map π_i, read in E, as a partial diffeomorphism of the complement of the exceptional hyperplane {u_i = 0} onto the complement of {x_i = 0}, with inverse blowUpChartInv.

Equations

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

noncomputable def Manifold.BlowUpGlue.offCenterDiffeo {𝕜 : 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 : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (Glued ψ Y c) M ⊤

The blow-down restricted to the points of a piece off the exceptional hyperplane, as a partial diffeomorphism onto the points of the chart off the centre: in the chart it is φ⁻¹ ∘ ψ⁻¹ ∘ π_i ∘ ψ, with inverse (chart)⁻¹ ∘ ψ⁻¹ ∘ blowUpChartInv ∘ ψ ∘ φ.

Equations

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

theorem Manifold.BlowUpGlue.isLocalDiffeomorphAt_gluedProj {𝕜 : 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 : ℕ} (j : PieceIdx ψ Y c) (hj : (pieceSet j).Nonempty) (u : ↑(pieceSet j)) (hu : ↑u ((pieceEmb j) j.2) ≠ 0) : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ gluedProj (toGlued j u)

The blow-down is a local diffeomorphism at every point of a piece off the exceptional hyperplane.

theorem Manifold.BlowUpGlue.isLocalDiffeomorphOn_gluedProj {𝕜 : 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 : ℕ} : IsLocalDiffeomorphOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ gluedProj (gluedProj ⁻¹' Yᶜ)

The blow-down is a local diffeomorphism off the exceptional divisor (towards condition (1) of [BM88, Definition 4.1]).

theorem Manifold.BlowUpGlue.toGlued_eq_of_gluedProj_eq {𝕜 : 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 : ℕ} {j j' : PieceIdx ψ Y c} (u : ↑(pieceSet j)) (u' : ↑(pieceSet j')) (hu' : ↑u' ((pieceEmb j') j'.2) ≠ 0) (hpq : blowDown j ↑u = blowDown j' ↑u') : toGlued j u = toGlued j' u'

Two points of pieces off the exceptional divisor over the same point of M coincide.

theorem Manifold.BlowUpGlue.bijOn_gluedProj {𝕜 : 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 : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (σ₀ : Fin c ↪ Fin n) (i₀ : Fin c) : Set.BijOn gluedProj (gluedProj ⁻¹' Yᶜ) Yᶜ

The blow-down is a bijection from the complement of the exceptional divisor onto M ∖ Y (condition (1) of [BM88, Definition 4.1]).