The blow-down of the glued space and the blow-up charts #
For the glued space Glued ψ Y c and its blow-down gluedProj:
- pieces over the same adapted chart are glued by the transition maps
T_ikof the local model, and a point of a piece over the chartφ'lies in the transition domain towards some piece overφ'(the direction vector of the lift is nonzero); - a point of a piece lies over the centre exactly when its scaling coordinate vanishes;
- every point of
Mlies under some piece (given adapted charts at every point: those of the closed submanifoldYat the points ofY, the translated charts ofHironaka.Manifold.BlowUp.AtlasoffY), so the blow-down is surjective; - the blow-down is analytic (in the chart of a piece it is
φ⁻¹ ∘ ψ⁻¹ ∘ π_i ∘ ψ); - the chart of a piece is a blow-up chart in the sense of
IsBlowUpChart, condition (2) of [BM88, Definition 4.1] in coordinates, and every adapted chart and every index has one, the blow-up charts over an adapted chart covering the preimage of its source (the clausesIsBlowUp.exists_chartandIsBlowUp.cover).
Together with Hironaka.Manifold.BlowUp.GluedOffCenter (condition (1)) and
Hironaka.Manifold.BlowUp.GluedTopology (Hausdorff, second countable, proper), this shows
that the glued space is a blowing-up of M with centre Y (Hironaka.Manifold.BlowUp.Exists).
Pieces over the same chart #
theorem
Manifold.BlowUpGlue.pieceChart_mk
{𝕜 : 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 : ℕ}
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
(k k' : Fin c)
:
Two pieces over the same adapted chart have the same chart.
theorem
Manifold.BlowUpGlue.pieceEmb_mk
{𝕜 : 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 : ℕ}
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
(k k' : Fin c)
:
Two pieces over the same adapted chart have the same block indices.
theorem
Manifold.BlowUpGlue.transDir_same
{𝕜 : 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 : ℕ}
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
(k k' : Fin c)
{u : Fin n → 𝕜}
(hu : u ∈ pieceSet (s, k))
(hkk' : k' ≠ k)
:
Between two pieces over the same chart the direction quotient is the ratio coordinate.
theorem
Manifold.BlowUpGlue.mem_transDom_same
{𝕜 : 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 : ℕ}
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
(k k' : Fin c)
{u : Fin n → 𝕜}
(hkk' : k' ≠ k)
:
The transition domain between two pieces over the same chart is {u_{k'} ≠ 0} inside the piece
set.
theorem
Manifold.BlowUpGlue.transMap_same
{𝕜 : 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 : ℕ}
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
(k k' : Fin c)
{u : Fin n → 𝕜}
(hu : u ∈ transDom (s, k) (s, k'))
:
Between two pieces over the same chart the transition map is the transition map T_ik of the
local model.
theorem
Manifold.BlowUpGlue.exists_mem_transDom
{𝕜 : 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}
{u : Fin n → 𝕜}
(hu : u ∈ pieceSet j)
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
(hs : blowDown j u ∈ (pieceChart (s, j.2)).source)
:
A point of a piece over the chart of another piece lies in the transition domain towards some
piece over that chart: the direction vector of the lift is nonzero (exists_liftDir_ne_zero).
theorem
Manifold.BlowUpGlue.exists_toGlued_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 : ℕ}
(p : Glued ψ Y c)
(s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c))
{k₀ : Fin c}
(hs : gluedProj p ∈ (pieceChart (s, k₀)).source)
:
Every point of the glued space over the chart of a piece lies in the image of a piece over that chart.
The blow-down and the centre #
theorem
Manifold.BlowUpGlue.gluedProj_mem_iff
{𝕜 : 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)
(u : ↑(pieceSet j))
:
A point of a piece lies over the centre exactly when its scaling coordinate vanishes.
theorem
Manifold.BlowUpGlue.gluedProj_notMem_iff
{𝕜 : 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)
(u : ↑(pieceSet j))
:
A point of piece j blows down off the centre iff its scaling coordinate is nonzero.
theorem
Manifold.BlowUpGlue.pieceChange_pieceMap_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'))
(h : blowDown j ↑u = blowDown j' ↑u')
:
The coordinate change between two pieces carries the chart map of a point to the chart map
of any point of the other piece over the same point of M.
Surjectivity of the blow-down #
theorem
Manifold.BlowUpGlue.exists_piece_mem_source
{𝕜 : 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)
(a : M)
:
∃ (s : Shrink.{u, max u_1 u} (AdaptedChart ψ Y c)), a ∈ (pieceChart (s, i₀)).source
Every point of M lies in the chart of a piece: an adapted chart of the closed submanifold at
a point of Y, a translated chart (exists_isAdaptedChart_of_notMem) off Y.
theorem
Manifold.BlowUpGlue.exists_blowDown_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 : ℕ}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M]
(hY : IsClosedSubmanifold ψ Y c)
(σ₀ : Fin c ↪ Fin n)
(i₀ : Fin c)
(a : M)
:
Every point of M lies under some piece.
theorem
Manifold.BlowUpGlue.gluedProj_surjective
{𝕜 : 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)
:
The blow-down of the glued space is onto M.
theorem
Manifold.BlowUpGlue.nonempty_glued
{𝕜 : 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)
[Nonempty M]
:
The glued space is nonempty when M is.
Analyticity of the blow-down #
theorem
Manifold.BlowUpGlue.contMDiffOn_gluedProj_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 : ℕ}
(j : PieceIdx ψ Y c)
(hj : (pieceSet j).Nonempty)
:
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ gluedProj (Set.range (toGlued j))
theorem
Manifold.BlowUpGlue.contMDiff_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 : ℕ}
:
ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ gluedProj
The blow-down is analytic.
Condition (2) of the definition: the blow-up charts #
theorem
Manifold.BlowUpGlue.isBlowUpChart_gluedChart
{𝕜 : 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)
:
IsBlowUpChart ψ gluedProj (pieceChart j) (pieceEmb j) j.2 (gluedChart j hj)
The chart of a piece is a blow-up chart of its index over its adapted chart.
theorem
Manifold.BlowUpGlue.exists_mem_maximalAtlas_source_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}
{c : ℕ}
[Nonempty (Glued ψ Y c)]
:
A chart of the maximal atlas with empty source and target.
theorem
Manifold.BlowUpGlue.exists_isBlowUpChart
{𝕜 : 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 : ℕ}
[Nonempty (Glued ψ Y c)]
{φ : OpenPartialHomeomorph M E}
{σ : Fin c ↪ Fin n}
(hφ : IsAdaptedChart ψ Y φ σ)
(i : Fin c)
:
∃ (Φ : OpenPartialHomeomorph (Glued ψ Y c) E), IsBlowUpChart ψ gluedProj φ σ i Φ
Condition (2) of [BM88, Definition 4.1]: every adapted chart and every index has a blow-up chart.
theorem
Manifold.BlowUpGlue.exists_isBlowUpChart_mem_source
{𝕜 : 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}
(hφ : IsAdaptedChart ψ Y φ σ)
(p : Glued ψ Y c)
(hp : gluedProj p ∈ φ.source)
:
∃ (i : Fin c) (Φ : OpenPartialHomeomorph (Glued ψ Y c) E), IsBlowUpChart ψ gluedProj φ σ i Φ ∧ p ∈ Φ.source
Condition (2) of [BM88, Definition 4.1]: the blow-up charts over an adapted chart cover the preimage of its source.