Uniqueness of the blowing-up up to a unique diffeomorphism #
Conditions (1) and (2) of [BM88, Definition 4.1] define the blowing-up π : M' → M uniquely, up
to an isomorphism of M' commuting with π. For two blowings-up π₁ : M₁' → M, π₂ : M₂' → M
of M with centre Y:
- uniqueness of lifts: two continuous maps
G, G' : N → M₂'(N ⊆ M₁'open) withπ₂ ∘ G = π₂ ∘ G' = π₁agree: off the exceptional divisorπ₂is injective, and the complement of the divisor is dense (in a blow-up chart it is{u_i ≠ 0}); - the lift:
g pis the unique point overπ₁ poff the divisor whenπ₁ p ∉ Y, andΦ₂⁻¹(Φ₁ p)for blow-up chartsΦ₁,Φ₂of the same index over one adapted chart atπ₁ pwhenπ₁ p ∈ Y(their targets coincide: the full model chart domain); near every pointgis given by such a chart formula (by uniqueness of lifts), so it is analytic; the lift in the other direction is a two-sided inverse (uniqueness of lifts again), and any diffeomorphism commuting with the blow-downs equalsg.
The uniqueness statement is IsBlowUp.exists_unique_diffeomorph; the source states it without
proof. It is what allows the blowing-up to be transported along isomorphisms
(Hironaka.Manifold.BlowUp.Functor).
Blow-up charts of one index over one adapted chart #
theorem
Manifold.IsBlowUpChart.target_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{c : ℕ}
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
{φ : OpenPartialHomeomorph M E}
{σ : Fin c ↪ Fin n}
{i : Fin c}
{Φ₁ : OpenPartialHomeomorph M₁' E}
{Φ₂ : OpenPartialHomeomorph M₂' E}
(hΦ₁ : IsBlowUpChart ψ π₁ φ σ i Φ₁)
(hΦ₂ : IsBlowUpChart ψ π₂ φ σ i Φ₂)
:
Two blow-up charts of the same index over one adapted chart have the same target.
theorem
Manifold.IsBlowUpChart.blowDown_symm_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{c : ℕ}
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
{φ : OpenPartialHomeomorph M E}
{σ : Fin c ↪ Fin n}
{i : Fin c}
{Φ₁ : OpenPartialHomeomorph M₁' E}
{Φ₂ : OpenPartialHomeomorph M₂' E}
(hΦ₁ : IsBlowUpChart ψ π₁ φ σ i Φ₁)
(hΦ₂ : IsBlowUpChart ψ π₂ φ σ i Φ₂)
{p : M₁'}
(hp : p ∈ Φ₁.source)
:
Φ₂⁻¹ ∘ Φ₁ lifts π₁ to π₂.
theorem
Manifold.IsBlowUpChart.contMDiffOn_symm_comp
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{c : ℕ}
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
{φ : OpenPartialHomeomorph M E}
{σ : Fin c ↪ Fin n}
{i : Fin c}
{Φ₁ : OpenPartialHomeomorph M₁' E}
{Φ₂ : OpenPartialHomeomorph M₂' E}
(hΦ₁ : IsBlowUpChart ψ π₁ φ σ i Φ₁)
(hΦ₂ : IsBlowUpChart ψ π₂ φ σ i Φ₂)
:
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑Φ₂.symm ∘ ↑Φ₁) Φ₁.source
The chart change Φ₂⁻¹ ∘ Φ₁ between blow-up charts of the same index over the same adapted
chart, for two blowings-up, is analytic on Φ₁.source (both charts read the same coordinates).
Density of the complement of the divisor and uniqueness of lifts #
theorem
Manifold.IsBlowUp.dense_preimage_compl
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
{π₁ : M₁' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h : IsBlowUp ψ Y c π₁)
:
The complement of the exceptional divisor is dense: in a blow-up chart it is {u_i ≠ 0}.
theorem
Manifold.IsBlowUp.eqOn_of_comp_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
{N : Set M₁'}
(hN : IsOpen N)
{G G' : M₁' → M₂'}
(hG : ContinuousOn G N)
(hG' : ContinuousOn G' N)
(hπ : ∀ p ∈ N, π₂ (G p) = π₁ p)
(hπ' : ∀ p ∈ N, π₂ (G' p) = π₁ p)
:
Set.EqOn G G' N
Uniqueness of lifts: two continuous maps over π₁ into the second blowing-up agree on an open
set.
The lift #
noncomputable def
Manifold.adChart
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
(hY : IsClosedSubmanifold ψ Y c)
{a : M}
(ha : a ∈ Y)
:
An adapted chart at a point of the centre.
Equations
- Manifold.adChart hY ha = ⋯.choose
Instances For
noncomputable def
Manifold.adEmb
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
(hY : IsClosedSubmanifold ψ Y c)
{a : M}
(ha : a ∈ Y)
:
Its block embedding.
Equations
- Manifold.adEmb hY ha = ⋯.choose
Instances For
theorem
Manifold.adChart_spec
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
(hY : IsClosedSubmanifold ψ Y c)
{a : M}
(ha : a ∈ Y)
:
The chosen adapted chart at a point of Y contains it and is adapted.
noncomputable def
Manifold.bIdx
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
{π₁ : M₁' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(p : M₁')
(hp : π₁ p ∈ Y)
:
Fin c
The index of a blow-up chart of π₁ at p over the adapted chart.
Equations
- Manifold.bIdx hY h₁ p hp = ⋯.choose
Instances For
noncomputable def
Manifold.bChart₁
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
{π₁ : M₁' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(p : M₁')
(hp : π₁ p ∈ Y)
:
OpenPartialHomeomorph M₁' E
A blow-up chart of π₁ at p.
Equations
- Manifold.bChart₁ hY h₁ p hp = ⋯.choose
Instances For
theorem
Manifold.bChart₁_spec
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
{π₁ : M₁' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(p : M₁')
(hp : π₁ p ∈ Y)
:
The chosen blow-up chart of π₁ at p is a blow-up chart containing p.
noncomputable def
Manifold.bChart₂
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
(p : M₁')
(hp : π₁ p ∈ Y)
:
OpenPartialHomeomorph M₂' E
A blow-up chart of π₂ of the same index over the same adapted chart.
Equations
- Manifold.bChart₂ hY h₁ h₂ p hp = ⋯.choose
Instances For
theorem
Manifold.bChart₂_spec
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
(p : M₁')
(hp : π₁ p ∈ Y)
:
IsBlowUpChart ψ π₂ (adChart hY hp) (adEmb hY hp) (bIdx hY h₁ p hp) (bChart₂ hY h₁ h₂ p hp)
The chosen blow-up chart of π₂ over the same adapted chart and index is a blow-up chart.
noncomputable def
Manifold.liftPoint
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
(p : M₁')
:
M₂'
The lift of π₁ to π₂: over the centre Φ₂⁻¹ ∘ Φ₁ in blow-up charts of one index over one
adapted chart, off the centre the unique point of M₂' off the divisor over π₁ p.
Equations
- Manifold.liftPoint hY h₁ h₂ p = if hp : π₁ p ∈ Y then ↑(Manifold.bChart₂ hY h₁ h₂ p hp).symm (↑(Manifold.bChart₁ hY h₁ p hp) p) else Exists.choose ⋯
Instances For
theorem
Manifold.liftPoint_of_mem
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
{p : M₁'}
(hp : π₁ p ∈ Y)
:
Over the centre the lift is read through the chosen blow-up charts.
theorem
Manifold.liftPoint_of_notMem
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
{p : M₁'}
(hp : π₁ p ∉ Y)
:
Off the centre the lift is the unique preimage under π₂ of π₁ p.
theorem
Manifold.blowDown_liftPoint
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
(p : M₁')
:
The lift commutes with the blow-downs: π₂ ∘ liftPoint = π₁.
theorem
Manifold.liftPoint_eq_of_notMem
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
{p : M₁'}
(hp : π₁ p ∉ Y)
{q : M₂'}
(hq : π₂ q = π₁ p)
:
Off the centre, liftPoint is the unique point off the divisor over π₁ p.
theorem
Manifold.liftPoint_eqOn_of_mem
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
{p : M₁'}
(hp : π₁ p ∈ Y)
:
Near a point over the centre, the lift is the chart formula Φ₂⁻¹ ∘ Φ₁.
theorem
Manifold.exists_eqOn_of_notMem
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
{p : M₁'}
(hp : π₁ p ∉ Y)
:
Near a point off the centre, the lift is Ψ⁻¹ ∘ π₁ for a local inverse Ψ of π₂.
theorem
Manifold.contMDiff_liftPoint
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
:
ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (liftPoint hY h₁ h₂)
The lift is analytic.
theorem
Manifold.liftPoint_liftPoint
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
(p : M₁')
:
The lift is a two-sided inverse of the lift in the other direction.
Uniqueness up to a unique diffeomorphism #
noncomputable def
Manifold.IsBlowUp.diffeomorph
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
:
Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤
The diffeomorphism between two blowings-up of M with centre Y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Manifold.IsBlowUp.exists_unique_diffeomorph
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
{Y : Set M}
{c : ℕ}
[ChartedSpace E M]
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
{π₁ : M₁' → M}
{π₂ : M₂' → M}
(hY : IsClosedSubmanifold ψ Y c)
(h₁ : IsBlowUp ψ Y c π₁)
(h₂ : IsBlowUp ψ Y c π₂)
:
∃! g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤, ∀ (p : M₁'), π₂ (g p) = π₁ p
Two blowings-up of M with centre Y are isomorphic over M by a unique diffeomorphism
[BM88, Definition 4.1].