Functoriality of the blowing-up under local isomorphisms #
An analytic isomorphism g between open subsets U₁ ⊆ M₁, U₂ ⊆ M₂ carrying Y₁ ∩ U₁ onto
Y₂ ∩ U₂ lifts to a unique analytic isomorphism π₁⁻¹(U₁) → π₂⁻¹(U₂) over g between
blowings-up with centres Y₁, Y₂ (IsBlowUp.exists_lift_partialDiffeomorph). This is the
functoriality of the blowing-up under local isomorphisms, the case of an isomorphism onto an open
subset of the pull-back of a blow-up along a smooth morphism [Kol07, Definition 30, 30.1]; it
follows from the uniqueness clause of [BM88, Definition 4.1]. The lift is built as in
Hironaka.Manifold.BlowUp.Unique: over the centre by blow-up charts of one index over an
adapted chart φ₁ of Y₁ at π₁ p and its transport φ₁ ∘ g⁻¹ (an adapted chart of Y₂), off
the centre as the unique point off the divisor over g(π₁ p); uniqueness of lifts (density of
the complement of the divisor, injectivity of π₂ off Y₂) gives the local chart formulas, the
inverse and the uniqueness clause. The first ingredient is that a chart of the maximal atlas
composed with the inverse of a partial diffeomorphism is a chart of the maximal atlas of the
target (transportChart, Hironaka/Manifold/Chart/Transport.lean). The centres are required to
have positive codimension: for c = 0 no total map M₁' → M₂' need exist.
This functoriality is what makes the blowing-up, and the sequences of blowings-up built from it,
compatible with local isomorphisms of the ambient manifold
(Hironaka.Manifold.FiniteSuccession.Lift,
Hironaka.Manifold.FiniteSuccession.Restrict.Transport).
The lift of a partial diffeomorphism carrying the centres to each other #
theorem
Manifold.IsBlowUpChart.blowDown_symm_apply_transport
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
{φ : OpenPartialHomeomorph M₁ E}
{σ : Fin c ↪ Fin n}
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
{i : Fin c}
{Φ₁ : OpenPartialHomeomorph M₁' E}
{Φ₂ : OpenPartialHomeomorph M₂' E}
(hsub : φ.source ⊆ g.source)
(hΦ₁ : IsBlowUpChart ψ π₁ φ σ i Φ₁)
(hΦ₂ : IsBlowUpChart ψ π₂ (transportChart g φ) σ i Φ₂)
{p : M₁'}
(hp : p ∈ Φ₁.source)
:
Φ₂⁻¹ ∘ Φ₁ lifts π₁ to π₂ over g, for blow-up charts of one index over an adapted chart
and its transport.
theorem
Manifold.IsBlowUpChart.contMDiffOn_symm_comp_transport
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
{φ : OpenPartialHomeomorph M₁ E}
{σ : Fin c ↪ Fin n}
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
{i : Fin c}
{Φ₁ : OpenPartialHomeomorph M₁' E}
{Φ₂ : OpenPartialHomeomorph M₂' E}
(hsub : φ.source ⊆ g.source)
(hΦ₁ : IsBlowUpChart ψ π₁ φ σ i Φ₁)
(hΦ₂ : IsBlowUpChart ψ π₂ (transportChart g φ) σ i Φ₂)
:
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑Φ₂.symm ∘ ↑Φ₁) Φ₁.source
The chart change between a blow-up chart of π₁ over φ and a blow-up chart of π₂ over the
transported chart is analytic on the source (the two charts read the same coordinates through g).
theorem
Manifold.IsBlowUp.eqOn_of_comp_eq_of_image_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
{N : Set M₁'}
(hN : IsOpen N)
(hNs : N ⊆ π₁ ⁻¹' g.source)
{G G' : M₁' → M₂'}
(hG : ContinuousOn G N)
(hG' : ContinuousOn G' N)
(hπ : ∀ p ∈ N, π₂ (G p) = ↑g.toPartialEquiv (π₁ p))
(hπ' : ∀ p ∈ N, π₂ (G' p) = ↑g.toPartialEquiv (π₁ p))
:
Set.EqOn G G' N
Uniqueness of lifts over g: two continuous maps over g ∘ π₁ into the second blowing-up
agree on an open subset of π₁⁻¹(g.source).
The chart data at a point over the centre #
noncomputable def
Manifold.adChartG
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
{a : M₁}
(ha : a ∈ Y₁)
:
The adapted chart at a point of the centre, restricted to the source of g.
Equations
- Manifold.adChartG g hY₁ ha = (Manifold.adChart hY₁ ha).restrOpen g.source ⋯
Instances For
theorem
Manifold.adChartG_isAdaptedChart
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
{a : M₁}
(ha : a ∈ Y₁)
:
IsAdaptedChart ψ Y₁ (adChartG g hY₁ ha) (adEmb hY₁ ha)
The chosen adapted chart at a, cut down to g.source, is adapted to Y₁.
theorem
Manifold.adChartG_source_subset
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
{a : M₁}
(ha : a ∈ Y₁)
:
The cut-down adapted chart has source inside g.source.
theorem
Manifold.mem_adChartG_source
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
{a : M₁}
(hp : a ∈ g.source)
(ha : a ∈ Y₁)
:
A point of Y₁ ∩ g.source lies in the source of its cut-down adapted chart.
noncomputable def
Manifold.bIdxG
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
{π₁ : M₁' → M₁}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
Fin c
The index of a blow-up chart of π₁ at p.
Equations
- Manifold.bIdxG g hY₁ h₁ hp hY = ⋯.choose
Instances For
noncomputable def
Manifold.bChart₁G
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
{π₁ : M₁' → M₁}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
OpenPartialHomeomorph M₁' E
A blow-up chart of π₁ at p.
Equations
- Manifold.bChart₁G g hY₁ h₁ hp hY = ⋯.choose
Instances For
theorem
Manifold.bChart₁G_spec
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
{M₁' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
{π₁ : M₁' → M₁}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
The chosen blow-up chart of π₁ at p over the cut-down adapted chart is a blow-up chart
containing p.
noncomputable def
Manifold.bChart₂G
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
{p : M₁'}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
OpenPartialHomeomorph M₂' E
A blow-up chart of π₂ of the same index over the transported adapted chart.
Equations
- Manifold.bChart₂G g hg hY₁ h₁ h₂ hp hY = ⋯.choose
Instances For
theorem
Manifold.bChart₂G_spec
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
{p : M₁'}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
IsBlowUpChart ψ π₂ (transportChart g (adChartG g hY₁ hY)) (adEmb hY₁ hY) (bIdxG g hY₁ h₁ hp hY)
(bChart₂G g hg hY₁ h₁ h₂ hp hY)
The chosen blow-up chart of π₂ over the transported chart (same block indices and index) is a
blow-up chart.
noncomputable def
Manifold.liftPointG
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
(p : M₁')
:
M₂'
The lift of π₁ to π₂ over g: over the centre Φ₂⁻¹ ∘ Φ₁ in blow-up charts of one index
over an adapted chart and its transport, off the centre the unique point of M₂' off the divisor
over g (π₁ p); an arbitrary point outside π₁⁻¹(g.source).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Manifold.liftPointG_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₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
Over the centre the lift of g is read through the chosen blow-up charts.
theorem
Manifold.blowDown_liftPointG
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
{p : M₁'}
(hp : π₁ p ∈ g.source)
:
The lift commutes with the blow-downs over g: π₂ ∘ liftPointG = g ∘ π₁ on π₁⁻¹(g.source).
theorem
Manifold.liftPointG_eq_of_notMem
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∉ Y₁)
{q : M₂'}
(hq : π₂ q = ↑g.toPartialEquiv (π₁ p))
:
Off the centre, the lift is the unique point off the divisor over g (π₁ p).
theorem
Manifold.liftPointG_eqOn_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₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∈ Y₁)
:
Near a point over the centre, the lift is the chart formula Φ₂⁻¹ ∘ Φ₁.
theorem
Manifold.exists_eqOn_of_notMem_G
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
{p : M₁'}
(hp : π₁ p ∈ g.source)
(hY : π₁ p ∉ Y₁)
:
∃ (N : Set M₁'),
IsOpen N ∧ p ∈ N ∧ N ⊆ π₁ ⁻¹' g.source ∧ ∃ (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₂' M₂ ⊤),
(∀ r ∈ N, ↑g.toPartialEquiv (π₁ r) ∈ Ψ.target) ∧ Set.EqOn (liftPointG g hg hY₁ h₁ h₂) (Ψ.invFun ∘ ↑g.toPartialEquiv ∘ π₁) N
Near a point off the centre, the lift is Ψ⁻¹ ∘ g ∘ π₁ for a local inverse Ψ of π₂.
theorem
Manifold.contMDiffOn_liftPointG
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
:
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (liftPointG g hg hY₁ h₁ h₂) (π₁ ⁻¹' g.source)
The lift is analytic on π₁⁻¹(g.source).
theorem
Manifold.liftPointG_mem_preimage
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
{p : M₁'}
(hp : π₁ p ∈ g.source)
:
The lift of g maps π₁⁻¹(g.source) into π₂⁻¹(g.target).
The lift as a partial diffeomorphism #
theorem
Manifold.liftPointG_liftPointG_symm
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
[Nonempty M₁']
(hY₂ : IsClosedSubmanifold ψ Y₂ c)
{p : M₁'}
(hp : π₁ p ∈ g.source)
:
The lift in the other direction inverts the lift on π₁⁻¹(g.source) (uniqueness of lifts of
π₁ to itself).
noncomputable def
Manifold.liftPartialDiffeomorph
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M₁ : Type u}
[TopologicalSpace M₁]
[ChartedSpace E M₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
{M₁' M₂' : Type u}
[TopologicalSpace M₁']
[ChartedSpace E M₁']
[TopologicalSpace M₂']
[ChartedSpace E M₂']
{π₁ : M₁' → M₁}
{π₂ : M₂' → M₂}
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁']
[T2Space M₁']
[SecondCountableTopology M₁']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂']
[T2Space M₂']
[SecondCountableTopology M₂']
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₁]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
[Nonempty M₂']
[Nonempty M₁']
(hY₂ : IsClosedSubmanifold ψ Y₂ c)
:
PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤
The lift of g as a partial diffeomorphism M₁' → M₂' with source π₁⁻¹(g.source) and
target π₂⁻¹(g.target).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Functoriality under local isomorphisms #
theorem
Manifold.IsBlowUp.exists_lift_partialDiffeomorph
{𝕜 : 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₁]
{M₂ : Type u}
[TopologicalSpace M₂]
[ChartedSpace E M₂]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M₂]
{Y₁ : Set M₁}
{Y₂ : Set M₂}
{c : ℕ}
{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₂}
(hc : 0 < c)
(hY₁ : IsClosedSubmanifold ψ Y₁ c)
(hY₂ : IsClosedSubmanifold ψ Y₂ c)
(h₁ : IsBlowUp ψ Y₁ c π₁)
(h₂ : IsBlowUp ψ Y₂ c π₂)
(g : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁ M₂ ⊤)
(hg : ↑g.toPartialEquiv '' (Y₁ ∩ g.source) = Y₂ ∩ g.target)
:
∃ (g' : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤),
g'.source = π₁ ⁻¹' g.source ∧ g'.target = π₂ ⁻¹' g.target ∧ (∀ p ∈ g'.source, π₂ (↑g'.toPartialEquiv p) = ↑g.toPartialEquiv (π₁ p)) ∧ ∀ (g'' : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M₁' M₂' ⊤),
g''.source = π₁ ⁻¹' g.source →
(∀ p ∈ g''.source, π₂ (↑g''.toPartialEquiv p) = ↑g.toPartialEquiv (π₁ p)) →
Set.EqOn (↑g''.toPartialEquiv) (↑g'.toPartialEquiv) g'.source
Functoriality under local isomorphisms: an analytic isomorphism g between open subsets
with g(Y₁ ∩ U₁) = Y₂ ∩ U₂ lifts to an analytic isomorphism π₁⁻¹(U₁) → π₂⁻¹(U₂) over g,
unique as a map on π₁⁻¹(U₁); the centres have positive codimension. This is the pull-back of a
blow-up along an isomorphism onto an open subset [Kol07, Definition 30, 30.1], and the uniqueness
is that of [BM88, Definition 4.1].