The lift of a local analytic isomorphism to the blowings-up #
The pull-back of a blow-up sequence along a smooth morphism h : Y → X has the stages
X_i ×_X Y and the centres Z_i ×_X Y; if h is surjective the pull-back determines the
sequence, while for a non-surjective h the pull-back may contain empty blow-ups, and the
information about the centres above X ∖ h(Y) is lost [Kol07, 30.1]. On analytic
manifolds the fibre product X_i ×_X Y along a local analytic isomorphism is replaced by the
blowing-up of the preimage centre h_i^{-1}(Z_i), which is identified with it by the uniqueness of
the blowing-up [BM88, Definition 4.1] (a local analytic isomorphism is flat, and blowing up
commutes with flat base change). The preimage h⁻¹(Y) of a closed submanifold of codimension c
under a local analytic isomorphism h : N → M is a closed submanifold of codimension c
(IsClosedSubmanifold.preimage_of_isLocalDiffeomorph, Hironaka/Manifold/Chart/Transport.lean).
This module provides the one-step lemmas, on manifolds that are not bundled:
blowUpLift: for blowings-upπ : M' → MofMalongYandπ' : N' → NofNalongh⁻¹(Y), the lifth' : N' → M'ofhover the blow-downs,π ∘ h' = h ∘ π'(blowDown_blowUpLift): the liftsliftPointGof the local inverses ofhto the blowings-up, glued (well defined by the uniqueness of lifts,IsBlowUp.eqOn_of_comp_eq_of_image_eq); it is a local analytic isomorphism (isLocalDiffeomorph_blowUpLift);- for any continuous
G : N' → M'overh(in particular the lift):Gagrees with the lift of every local inverseΦofhonπ'⁻¹(Φ.source)(eqOn_liftPartialDiffeomorph_of_comm), is surjective whenhis (surjective_of_comm), injective whenhis (injective_of_comm), and an open embedding whenhis (isOpenEmbedding_of_comm, for a local analytic isomorphismG).
The empty cases need no positive-codimension proviso: a point of N' over h (π' q) produces a
point of M' (exists_blowDown_eq_apply), and conversely a point of M' over h b produces a
point of N' over b (exists_blowDown_eq_of_blowDown_eq), through the blow-up charts (which
exist exactly where the codimension is positive) off and on the centre.
These lemmas are the steps of the pull-back of a whole sequence of centres in CenterList.lean
(BlowUpSequence.pullback).
The lift of a local analytic isomorphism to the blowings-up #
theorem
Manifold.exists_blowDown_eq_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ : E ≃L[𝕜] Fin n → 𝕜}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace E M]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
(q : N')
:
∃ (p : M'), π p = h (π' q)
Over the image h (π' q) of a point of N' lies a point of M': off the centre by the
bijection off the exceptional divisor, on the centre through a blow-up chart (whose existence,
IsBlowUp.cover, forces the codimension to be positive) and the surjectivity of π.
theorem
Manifold.exists_blowDown_eq_of_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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
(b : N)
{p : M'}
(hp : π p = h b)
:
∃ (q : N'), π' q = b
Over a point b of N whose image h b is a blow-down lies a point of N' (the converse of
exists_blowDown_eq_apply, by the same case distinction).
noncomputable def
Manifold.blowUpLiftAux
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
[Nonempty M']
(q : N')
:
M'
The lift of h to the blowings-up, glued from the lifts liftPointG of the chosen local
inverses of h at the blow-downs of the points (Classical.choose on
(hh (π' q)).exists_partialDiffeomorph, the partial diffeomorphism agreeing with h near
π' q).
Equations
- Manifold.blowUpLiftAux hY hh hπ hπ' q = Manifold.liftPointG ⋯.choose ⋯ ⋯ hπ' hπ q
Instances For
theorem
Manifold.liftPointG_eq_liftPointG
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
[Nonempty M']
{Φ Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N M ⊤}
(hΦ : Set.EqOn h (↑Φ.toPartialEquiv) Φ.source)
(hΨ : Set.EqOn h (↑Ψ.toPartialEquiv) Ψ.source)
{q : N'}
(hqΦ : π' q ∈ Φ.source)
(hqΨ : π' q ∈ Ψ.source)
:
The lifts of two local inverses of h agree at a point over both sources (uniqueness of
lifts, IsBlowUp.eqOn_of_comp_eq_of_image_eq on π'⁻¹(Φ.source ∩ Ψ.source)).
theorem
Manifold.blowUpLiftAux_eq
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
[Nonempty M']
{Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N M ⊤}
(hΦ : Set.EqOn h (↑Φ.toPartialEquiv) Φ.source)
{q : N'}
(hq : π' q ∈ Φ.source)
:
The glued lift agrees with the lift of any local inverse Φ of h over Φ.source.
theorem
Manifold.blowDown_blowUpLiftAux
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
[Nonempty M']
(q : N')
:
The glued lift lies over h: π ∘ h' = h ∘ π'.
theorem
Manifold.isLocalDiffeomorph_blowUpLiftAux
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
[Nonempty M']
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (blowUpLiftAux hY hh hπ hπ')
The glued lift is a local analytic isomorphism: at q₀ it agrees with the partial
diffeomorphism liftPartialDiffeomorph lifting the local inverse chosen at π' q₀.
theorem
Manifold.exists_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
:
∃ (h' : N' → M'),
(∀ (q : N'), π (h' q) = h (π' q)) ∧ IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h'
A local analytic isomorphism h : N → M lifts to a local analytic isomorphism h' : N' → M'
of the blowings-up of N along h⁻¹(Y) and of M along Y, over the blow-downs (the lifts of
the local inverses, glued). If M' is empty so is N', and the lift is the empty map.
noncomputable def
Manifold.blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
:
N' → M'
The lift h' : N' → M' of a local analytic isomorphism h : N → M to the blowings-up of
N along h⁻¹(Y) and of M along Y, over the blow-downs (π ∘ h' = h ∘ π',
blowDown_blowUpLift): the lifts of the local inverses of h, glued (chosen from
exists_blowUpLift). It plays the role of the map X_{i+1} ×_X Y → X_{i+1} of the pull-back
[Kol07, 30.1].
Equations
- Manifold.blowUpLift hY hh hπ hπ' = ⋯.choose
Instances For
theorem
Manifold.blowDown_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
(q : N')
:
The lift lies over h: π ∘ h' = h ∘ π', the commutative square of the pull-back.
theorem
Manifold.isLocalDiffeomorph_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
:
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (blowUpLift hY hh hπ hπ')
The lift is a local analytic isomorphism.
theorem
Manifold.contMDiff_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
:
ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (blowUpLift hY hh hπ hπ')
The lift is analytic.
Properties transferred from h to any map over h (uniqueness of lifts) #
theorem
Manifold.eqOn_liftPartialDiffeomorph_of_comm
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
{G : N' → M'}
[Nonempty N']
[Nonempty M']
(hG : Continuous G)
(hGπ : ∀ (q : N'), π (G q) = h (π' q))
{Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N M ⊤}
(hΦ : Set.EqOn h (↑Φ.toPartialEquiv) Φ.source)
:
Set.EqOn G (↑(liftPartialDiffeomorph Φ ⋯ ⋯ hπ' hπ hY).toPartialEquiv) (π' ⁻¹' Φ.source)
A continuous map G : N' → M' over h agrees with the lift of every local inverse Φ of h
on π'⁻¹(Φ.source) (uniqueness of lifts).
theorem
Manifold.surjective_of_comm
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
{G : N' → M'}
(hs : Function.Surjective h)
(hG : Continuous G)
(hGπ : ∀ (q : N'), π (G q) = h (π' q))
:
A continuous map over a surjective h is surjective (the surjective case of
[Kol07, 30.1]): a point p of M' lies over h b, and the lift of the local
inverse of h at b maps π'⁻¹(Φ.source) onto π⁻¹(Φ.target) ∋ p.
theorem
Manifold.injective_of_comm
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
{G : N' → M'}
(hi : Function.Injective h)
(hG : Continuous G)
(hGπ : ∀ (q : N'), π (G q) = h (π' q))
:
A continuous map over an injective h is injective: two points with the same image lie over
the same b, and the lift of the local inverse at b is injective on π'⁻¹(Φ.source).
theorem
Manifold.isOpenEmbedding_of_comm
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
{G : N' → M'}
(he : Topology.IsOpenEmbedding h)
(hG : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ G)
(hGπ : ∀ (q : N'), π (G q) = h (π' q))
:
A local analytic isomorphism G over an open embedding h is an open embedding (the
open-embedding case, the second of the two situations in which a blow-up sequence functor is
required to commute with smooth morphisms [Kol07, 34.1]).
theorem
Manifold.surjective_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
(hs : Function.Surjective h)
:
Function.Surjective (blowUpLift hY hh hπ hπ')
The lift of a surjective local analytic isomorphism is surjective [Kol07, 30.1].
theorem
Manifold.injective_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
(hi : Function.Injective h)
:
Function.Injective (blowUpLift hY hh hπ hπ')
The lift of an injective local analytic isomorphism is injective.
theorem
Manifold.isOpenEmbedding_blowUpLift
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
(he : Topology.IsOpenEmbedding h)
:
Topology.IsOpenEmbedding (blowUpLift hY hh hπ hπ')
The lift of an open embedding is an open embedding (the open-embedding case of [Kol07, 34.1]).
theorem
Manifold.preimage_blowUpLift_preimage
{𝕜 : 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]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace E N]
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N]
{h : N → M}
{Y : Set M}
{c : ℕ}
{M' : Type u}
[TopologicalSpace M']
[ChartedSpace E M']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M']
[T2Space M']
[SecondCountableTopology M']
{N' : Type u}
[TopologicalSpace N']
[ChartedSpace E N']
[IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N']
[T2Space N']
[SecondCountableTopology N']
{π : M' → M}
{π' : N' → N}
(hY : IsClosedSubmanifold ψ Y c)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ h)
(hπ : IsBlowUp ψ Y c π)
(hπ' : IsBlowUp ψ (h ⁻¹' Y) c π')
:
The exceptional divisor pulls back: h'⁻¹(π⁻¹(Y)) = π'⁻¹(h⁻¹(Y)) (Kollár's F_{i+1} ×_X Y).