The blowing-up restricted to an open subset

The blowing-up commutes with restriction to open sets: for U ⊆ M open, π : π⁻¹(U) → U is the blowing-up of U with centre Y ∩ U. This is implicit in the uniqueness clause of [BM88, Definition 4.1], and it is the case of an open immersion of the pull-back of a blow-up along a smooth morphism [Kol07, Definition 30, 30.1]. Charts of an open subset U (Mathlib's Opens charted space: the restrictions subtypeRestr of the charts of M) and charts of M are exchanged along the inclusion: a chart of the maximal atlas of M restricts to one of U (subtypeRestr_mem_maximalAtlas_of_mem_maximalAtlas), and a chart of the maximal atlas of U extends along the inclusion to one of M (Opens.extendChart); adapted charts and blow-up charts are exchanged accordingly, and every clause of IsBlowUp descends (IsBlowUp.restrictOpens'). More generally an analytic map restricted to open submanifolds stays analytic (contMDiff_codRestrict_opens).

The restriction of a finite succession of blowings-up to an open subset (FiniteSuccession.restrict) is built from IsBlowUp.restrictOpens'.

Charts of an open subset and of the ambient space

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_symm_apply {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) {x : M} (hx : x ∈ s) : ↑(s.openPartialHomeomorphSubtypeCoe hs).symm x = ⟨x, hx⟩

The inverse of the inclusion chart of an open subset, at a point of the subset.

noncomputable def TopologicalSpace.Opens.extendChart {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) (φ : OpenPartialHomeomorph (↥s) H) : OpenPartialHomeomorph M H

A chart of an open subset s, extended along the inclusion to a chart of M: coe⁻¹ ≫ₕ φ.

Equations

• TopologicalSpace.Opens.extendChart hs φ = (s.openPartialHomeomorphSubtypeCoe hs).symm.trans φ

theorem TopologicalSpace.Opens.mem_extendChart_source_iff {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) (φ : OpenPartialHomeomorph (↥s) H) {x : M} : x ∈ (extendChart hs φ).source ↔ ∃ (hx : x ∈ s), ⟨x, hx⟩ ∈ φ.source

Membership in the source of the extended chart, unfolded.

theorem TopologicalSpace.Opens.extendChart_source_subset {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) (φ : OpenPartialHomeomorph (↥s) H) : (extendChart hs φ).source ⊆ ↑s

The source of the extended chart lies in the open set.

theorem TopologicalSpace.Opens.extendChart_apply {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) (φ : OpenPartialHomeomorph (↥s) H) {x : M} (hx : x ∈ s) : ↑(extendChart hs φ) x = ↑φ ⟨x, hx⟩

The extended chart agrees with the chart of the open subset.

theorem TopologicalSpace.Opens.extendChart_target {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) (φ : OpenPartialHomeomorph (↥s) H) : (extendChart hs φ).target = φ.target

The extended chart has the target of the chart it extends.

theorem Manifold.subtypeRestr_mem_maximalAtlas_of_mem_maximalAtlas {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) [ChartedSpace H M] {G : StructureGroupoid H} [HasGroupoid M G] [ClosedUnderRestriction G] {e : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M G) : e.subtypeRestr hs ∈ StructureGroupoid.maximalAtlas (↥s) G

Restricting a chart of the maximal atlas of M to an open subset yields a chart of the maximal atlas of the subset (Mathlib's StructureGroupoid.subtypeRestr_mem_maximalAtlas for the charts of the atlas).

theorem TopologicalSpace.Opens.extendChart_mem_maximalAtlas {H : Type u_1} [TopologicalSpace H] {M : Type u_2} [TopologicalSpace M] {s : Opens M} (hs : Nonempty ↥s) (φ : OpenPartialHomeomorph (↥s) H) [ChartedSpace H M] {G : StructureGroupoid H} [HasGroupoid M G] [ClosedUnderRestriction G] (hφ : φ ∈ StructureGroupoid.maximalAtlas (↥s) G) : extendChart hs φ ∈ StructureGroupoid.maximalAtlas M G

A chart of the maximal atlas of an open subset extends to a chart of the maximal atlas of M.

Analytic maps restricted to open submanifolds

theorem Manifold.contMDiff_codRestrict_opens {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} {E' : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] {f : N → M} (hf : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ f) {V : TopologicalSpace.Opens M} {W : TopologicalSpace.Opens N} {f' : ↥W → ↥V} (hf' : ∀ (p : ↥W), ↑(f' p) = f ↑p) : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ f'

An analytic map restricted to open submanifolds is analytic (contMDiff_restrict, for any analytic map).

Restriction of a blowing-up over an open subset

theorem Manifold.mem_opens_of_blowDown_mem {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {q : M'} (hq : π q ∈ U) : q ∈ U'

A point whose blow-down lies in U lies in U' = π⁻¹(U).

theorem Manifold.IsBlowUpChart.subtypeRestr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] {c : ℕ} {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (hU : Nonempty ↥U) (hU'ne : Nonempty ↥U') {φ : OpenPartialHomeomorph (↥U) E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π (TopologicalSpace.Opens.extendChart hU φ) σ i Φ) : IsBlowUpChart ψ π' φ σ i (Φ.subtypeRestr hU'ne)

The restriction of a blow-up chart to U' is a blow-up chart of the restricted blowing-up over the restricted adapted chart.

theorem Manifold.isAdaptedChart_extendChart {𝕜 : 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] {U : TopologicalSpace.Opens M} (hU : Nonempty ↥U) {φ : OpenPartialHomeomorph (↥U) E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ (Subtype.val ⁻¹' Y) φ σ) : IsAdaptedChart ψ Y (TopologicalSpace.Opens.extendChart hU φ) σ

An adapted chart of Y ∩ U on the open subset U extends to an adapted chart of Y.

theorem Manifold.IsBlowUp.surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (i₀ : Fin c) : Function.Surjective π

A blowing-up with a nonempty centre is surjective: a point of Y is the blow-down of the centre point of a blow-up chart.

theorem Manifold.contMDiff_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (h : IsBlowUp ψ Y c π) : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π'

The restricted blow-down is analytic.

theorem Manifold.continuous_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (h : IsBlowUp ψ Y c π) : Continuous π'

The restricted blow-down is continuous.

theorem Manifold.bijOn_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (h : IsBlowUp ψ Y c π) : Set.BijOn π' (π' ⁻¹' (Subtype.val ⁻¹' Y)ᶜ) (Subtype.val ⁻¹' Y)ᶜ

The restricted blow-down is a bijection off the restricted centre (condition (1) of [BM88, Definition 4.1] for π⁻¹(U) → U).

theorem Manifold.isProperMap_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) [T2Space M] (h : IsBlowUp ψ Y c π) : IsProperMap π'

The restricted blow-down is proper: a compact subset of U is compact in M, its preimage under π is compact and lies in π⁻¹(U).

theorem Manifold.isLocalDiffeomorphOn_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (h : IsBlowUp ψ Y c π) : IsLocalDiffeomorphOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π' (π' ⁻¹' (Subtype.val ⁻¹' Y)ᶜ)

The local diffeomorphism of π at a point off the divisor, restricted over U.

theorem Manifold.IsBlowUp.restrictOpens' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {M' : Type u} [TopologicalSpace M'] {π : M' → M} [ChartedSpace E M] {Y : Set M} {c : ℕ} [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) : IsBlowUp ψ (Subtype.val ⁻¹' Y) c π'

The blowing-up restricted over an open subset U is a blowing-up of U with centre Y ∩ U (the pull-back along the open immersion U → M, [Kol07, Definition 30, 30.1]).