The strict transform is the blowing-up of the submanifold

Kollár identifies the stage S_{i+1} := Bl_{Z_i ∩ S_i} S_i of a restricted blow-up sequence with the birational transform (π_i)⁻¹_* S_i ⊂ X_{i+1}, with a reference to Hartshorne [Kol07, Definition 30.2]. This module proves the manifold statement: for a blowing-up π : M' → M along Y ⊆ S, both closed submanifolds, the strict transform S' = closure (π⁻¹(S ∖ Y)) with the restricted blow-down π|_{S'} : S' → S is a blowing-up of the bundled S along Y in the sense of [BM88, Definition 4.1] (isBlowUp_restrictMap), and it is identified over S with the blowing-up Bl_Y S (BlowUpSpace, blowUp) by a diffeomorphism (exists_diffeomorph_restrictMap; unique by IsBlowUp.exists_unique_diffeomorph).

The proof is the lift construction of BlowUp/Unique.lean with the chart data supplied by the flag charts: IsBlowUp asks for blow-up charts over every adapted chart of Y in S, which the strict transform does not offer directly, so we first build the two lifts S' → Bl_Y S and Bl_Y S → S' over S. At a point over the centre both are read in one pair of blow-up charts of one index over one adapted chart of Y in S: the induced chart of a flag chart of M at the point (isAdaptedChart_chartOn_flag), over which S' has the induced charts of the ambient blow-up charts of index ∉ range τ (isBlowUpChart_chartOn_flag; the charts covering S_1 in [Kol07, Theorem 88, proof]) and Bl_Y S has charts by definition (exists_chart, cover). Off the centre both lifts are the unique preimage. The lifts are analytic (chart formulas over the centre, local inverses off it — Fields.lean's restriction of the ambient local inverse for the lift into S'), and inverse to each other by the uniqueness of lifts (eqOn_of_comp_eq_of_dense: two continuous lifts agree off the centre by injectivity there and extend by density, S' ∖ π⁻¹(Y) being dense in S' by the definition of S'). The resulting diffeomorphism transports IsBlowUp from Bl_Y S to S' (Transport.lean).

The hypotheses of one step are packaged in the Prop-structure RestrictBlowUpData; the two main statements at the end unpack it. Not in the sources beyond Kollár's remark; the proof is a chart construction.

Uniqueness of lifts, the general form

theorem Manifold.eqOn_of_comp_eq_of_dense {X : Type u_1} {X' : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace X'] [T2Space X'] {π₁ : X → Z} {π₂ : X' → Z} {T : Set Z} (hinj : Set.InjOn π₂ (π₂ ⁻¹' Tᶜ)) (hdense : Dense (π₁ ⁻¹' Tᶜ)) {N : Set X} (hN : IsOpen N) {G G' : X → X'} (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

Two continuous maps over π₁ into a space where π₂ is injective off T agree on an open set N, provided the points off T are dense in the source (the form of IsBlowUp.eqOn_of_comp_eq with the two inputs made explicit).

structure Manifold.RestrictBlowUpData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (ψ : E ≃L[𝕜] Fin n → 𝕜) (π : M' → M) (Y S : Set M) (c s : ℕ) : Prop

The data of one step of a restricted blow-up sequence [Kol07, Definition 30.2]: a blowing-up π : M' → M along a closed submanifold Y contained in a closed submanifold S (the ambient manifolds carry all the instances the construction needs).

• hS : IsClosedSubmanifold ψ S s
• hY : IsClosedSubmanifold ψ Y c
• isBlowUp : IsBlowUp ψ Y c π
• subset : Y ⊆ S

theorem Manifold.RestrictBlowUpData.hS' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : IsClosedSubmanifold ψ (strictTransformSet π Y S) s

The strict transform S' is a closed submanifold of M' of the codimension of S.

theorem Manifold.RestrictBlowUpData.mapsTo {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (x : M') : x ∈ strictTransformSet π Y S → π x ∈ S

π carries S' into S.

theorem Manifold.RestrictBlowUpData.hY' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⋯.preimageVal Y) (c - s)

The centre Y is a closed submanifold of the bundled S of codimension c − s.

@[reducible, inline]

abbrev Manifold.RestrictBlowUpData.blowDown {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : AnalyticMap ⋯.toAnalyticManifold ⋯.toAnalyticManifold

The restricted blow-down π|_{S'} : S' → S.

Equations

• D.blowDown = ⋯.restrictMap ⋯ π ⋯ ⋯

@[reducible, inline]

noncomputable abbrev Manifold.RestrictBlowUpData.space {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)

The blowing-up Bl_Y S of the bundled S along Y.

Equations

• D.space = Manifold.blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) ⋯

@[reducible, inline]

noncomputable abbrev Manifold.RestrictBlowUpData.proj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : AnalyticMap D.space ⋯.toAnalyticManifold

Its blow-down.

Equations

• D.proj = Manifold.blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) ⋯

theorem Manifold.RestrictBlowUpData.isBlowUp_proj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⋯.preimageVal Y) (c - s) ⇑D.proj

The chart data at a point of the centre

noncomputable def Manifold.RestrictBlowUpData.flagChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : OpenPartialHomeomorph M E

A flag chart of Y ⊆ S at a ∈ Y.

Equations

• D.flagChart ha = ⋯.choose

noncomputable def Manifold.RestrictBlowUpData.flagEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : Fin c ↪ Fin n

Its block embedding for Y.

Equations

• D.flagEmb ha = ⋯.choose

noncomputable def Manifold.RestrictBlowUpData.flagTau {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : Fin s ↪ Fin c

The S-indices among the centre indices.

Equations

• D.flagTau ha = ⋯.choose

theorem Manifold.RestrictBlowUpData.flagChart_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : a ∈ (D.flagChart ha).source ∧ IsAdaptedChart ψ Y (D.flagChart ha) (D.flagEmb ha) ∧ ∀ x ∈ (D.flagChart ha).source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑(D.flagChart ha) x) ((D.flagEmb ha) ((D.flagTau ha) j)) = 0

theorem Manifold.RestrictBlowUpData.isAdaptedChart_flagChart_S {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : IsAdaptedChart ψ S (D.flagChart ha) ((D.flagTau ha).trans (D.flagEmb ha))

The flag chart is adapted to S with the indices τ.trans σ.

noncomputable def Manifold.RestrictBlowUpData.flagChartS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : OpenPartialHomeomorph ⋯.toAnalyticManifold.carrier (Fin (n - s) → 𝕜)

The induced chart of the flag chart on the bundled S.

Equations

• D.flagChartS ha = ⋯.inducedChart ⋯ ⋯

theorem Manifold.RestrictBlowUpData.isAdaptedChart_flagChartS {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) : IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⋯.preimageVal Y) (D.flagChartS ha) (restrictEmb (D.flagEmb ha) (D.flagTau ha))

The induced chart is adapted to Y inside S, with the block restrictEmb σ τ.

theorem Manifold.RestrictBlowUpData.mem_flagChartS_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) {y : ⋯.toAnalyticManifold.carrier} (hy : ↑y ∈ (D.flagChart ha).source) : y ∈ (D.flagChartS ha).source

noncomputable def Manifold.RestrictBlowUpData.ambChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) (i : Fin c) : OpenPartialHomeomorph M' E

The ambient blow-up chart of an index over the flag chart (the clause exists_chart of IsBlowUp).

Equations

• D.ambChart ha i = ⋯.choose

theorem Manifold.RestrictBlowUpData.ambChart_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) (i : Fin c) : IsBlowUpChart ψ π (D.flagChart ha) (D.flagEmb ha) i (D.ambChart ha i)

theorem Manifold.RestrictBlowUpData.isAdaptedChart_S' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π (D.flagChart ha) (D.flagEmb ha) i Φ) (hi : i ∉ Set.range ⇑(D.flagTau ha)) : IsAdaptedChart ψ (strictTransformSet π Y S) Φ ((D.flagTau ha).trans (D.flagEmb ha))

An ambient blow-up chart of an index ∉ range τ over the flag chart is adapted to S'.

noncomputable def Manifold.RestrictBlowUpData.chartS' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π (D.flagChart ha) (D.flagEmb ha) i Φ) (hi : i ∉ Set.range ⇑(D.flagTau ha)) {p₀ : M'} (hp₀ : p₀ ∈ strictTransformSet π Y S) : OpenPartialHomeomorph ⋯.toAnalyticManifold.carrier (Fin (n - s) → 𝕜)

The induced chart of S' from an ambient blow-up chart of an index ∉ range τ.

Equations

• D.chartS' ha hΦ hi hp₀ = ⋯.inducedChart ⋯ hp₀

theorem Manifold.RestrictBlowUpData.isBlowUpChart_chartS' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π (D.flagChart ha) (D.flagEmb ha) i Φ) (hi : i ∉ Set.range ⇑(D.flagTau ha)) {p₀ : M'} (hp₀ : p₀ ∈ strictTransformSet π Y S) : IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑D.blowDown) (D.flagChartS ha) (restrictEmb (D.flagEmb ha) (D.flagTau ha)) (restrictIdx (D.flagTau ha) hi) (D.chartS' ha hΦ hi hp₀)

The induced chart of S' is a blow-up chart of the restricted blow-down over the induced chart of S.

theorem Manifold.RestrictBlowUpData.mem_chartS'_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π (D.flagChart ha) (D.flagEmb ha) i Φ) (hi : i ∉ Set.range ⇑(D.flagTau ha)) {p₀ : M'} (hp₀ : p₀ ∈ strictTransformSet π Y S) {p : ⋯.toAnalyticManifold.carrier} (hp : ↑p ∈ Φ.source) : p ∈ (D.chartS' ha hΦ hi hp₀).source

noncomputable def Manifold.RestrictBlowUpData.chartB {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) (i'' : Fin (c - s)) : OpenPartialHomeomorph D.space.carrier (Fin (n - s) → 𝕜)

The blow-up chart of Bl_Y S of an index over the induced flag chart.

Equations

• D.chartB ha i'' = ⋯.choose

theorem Manifold.RestrictBlowUpData.isBlowUpChart_chartB {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {a : M} (ha : a ∈ Y) (i'' : Fin (c - s)) : IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑D.proj) (D.flagChartS ha) (restrictEmb (D.flagEmb ha) (D.flagTau ha)) i'' (D.chartB ha i'')

The chart pair at a point of S' over the centre

noncomputable def Manifold.RestrictBlowUpData.fIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : Fin c

The index of an ambient blow-up chart at p over the flag chart at π p (the clause cover of IsBlowUp).

Equations

• D.fIdx p hp = ⋯.choose

noncomputable def Manifold.RestrictBlowUpData.fChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : OpenPartialHomeomorph M' E

An ambient blow-up chart at p.

Equations

• D.fChart p hp = ⋯.choose

theorem Manifold.RestrictBlowUpData.fChart_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : IsBlowUpChart ψ π (D.flagChart hp) (D.flagEmb hp) (D.fIdx p hp) (D.fChart p hp) ∧ ↑p ∈ (D.fChart p hp).source

theorem Manifold.RestrictBlowUpData.fIdx_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : D.fIdx p hp ∉ Set.range ⇑(D.flagTau hp)

Its index is not an S-index: S' misses those charts.

noncomputable def Manifold.RestrictBlowUpData.fChartS' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : OpenPartialHomeomorph ⋯.toAnalyticManifold.carrier (Fin (n - s) → 𝕜)

The induced blow-up chart of S' at p.

Equations

• D.fChartS' p hp = D.chartS' hp ⋯ ⋯ ⋯

theorem Manifold.RestrictBlowUpData.fChartS'_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑D.blowDown) (D.flagChartS hp) (restrictEmb (D.flagEmb hp) (D.flagTau hp)) (restrictIdx (D.flagTau hp) ⋯) (D.fChartS' p hp) ∧ p ∈ (D.fChartS' p hp).source

noncomputable def Manifold.RestrictBlowUpData.fChartB {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : OpenPartialHomeomorph D.space.carrier (Fin (n - s) → 𝕜)

The blow-up chart of Bl_Y S of the same index over the same induced chart.

Equations

• D.fChartB p hp = D.chartB hp (Manifold.restrictIdx (D.flagTau hp) ⋯)

theorem Manifold.RestrictBlowUpData.fChartB_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) (hp : π ↑p ∈ Y) : IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑D.proj) (D.flagChartS hp) (restrictEmb (D.flagEmb hp) (D.flagTau hp)) (restrictIdx (D.flagTau hp) ⋯) (D.fChartB p hp)

The chart pair at a point of Bl_Y S over the centre

noncomputable def Manifold.RestrictBlowUpData.rIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : Fin (c - s)

The index of a blow-up chart of Bl_Y S at q over the induced flag chart.

Equations

• D.rIdx q hq = ⋯.choose

noncomputable def Manifold.RestrictBlowUpData.rChartB {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : OpenPartialHomeomorph D.space.carrier (Fin (n - s) → 𝕜)

A blow-up chart of Bl_Y S at q.

Equations

• D.rChartB q hq = ⋯.choose

theorem Manifold.RestrictBlowUpData.rChartB_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑D.proj) (D.flagChartS hq) (restrictEmb (D.flagEmb hq) (D.flagTau hq)) (D.rIdx q hq) (D.rChartB q hq) ∧ q ∈ (D.rChartB q hq).source

noncomputable def Manifold.RestrictBlowUpData.rIdxAmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : Fin c

The ambient index of the chart of q.

Equations

• D.rIdxAmb q hq = ↑((Manifold.complEquiv (D.flagTau hq)).symm (D.rIdx q hq))

theorem Manifold.RestrictBlowUpData.rIdxAmb_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : D.rIdxAmb q hq ∉ Set.range ⇑(D.flagTau hq)

theorem Manifold.RestrictBlowUpData.restrictIdx_rIdxAmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : restrictIdx (D.flagTau hq) ⋯ = D.rIdx q hq

noncomputable def Manifold.RestrictBlowUpData.rChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : OpenPartialHomeomorph M' E

The ambient blow-up chart of that index over the flag chart.

Equations

• D.rChart q hq = D.ambChart hq (D.rIdxAmb q hq)

theorem Manifold.RestrictBlowUpData.rChart_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : IsBlowUpChart ψ π (D.flagChart hq) (D.flagEmb hq) (D.rIdxAmb q hq) (D.rChart q hq)

theorem Manifold.RestrictBlowUpData.symm_embedCompl_mem_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : ψ.symm (embedCompl ((D.flagTau hq).trans (D.flagEmb hq)) (↑(D.rChartB q hq) q)) ∈ (D.rChart q hq).target

The chart image of q, embedded on the coordinate subspace {u_{σ (τ j)} = 0}, lies in the target of the ambient chart.

noncomputable def Manifold.RestrictBlowUpData.rPoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : ⋯.toAnalyticManifold.carrier

The point of S' corresponding to q: the ambient chart's inverse on the coordinate subspace.

Equations

• D.rPoint q hq = ⟨↑(D.rChart q hq).symm (ψ.symm (Manifold.embedCompl ((D.flagTau hq).trans (D.flagEmb hq)) (↑(D.rChartB q hq) q))), ⋯⟩

noncomputable def Manifold.RestrictBlowUpData.rChartS' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : OpenPartialHomeomorph ⋯.toAnalyticManifold.carrier (Fin (n - s) → 𝕜)

The induced blow-up chart of S' of the index of q.

Equations

• D.rChartS' q hq = D.chartS' hq ⋯ ⋯ ⋯

theorem Manifold.RestrictBlowUpData.rChartS'_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) (hq : ↑(D.proj q) ∈ Y) : IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑D.blowDown) (D.flagChartS hq) (restrictEmb (D.flagEmb hq) (D.flagTau hq)) (D.rIdx q hq) (D.rChartS' q hq)

The lift S' → Bl_Y S

noncomputable def Manifold.RestrictBlowUpData.liftToBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) : D.space.carrier

The lift of the restricted blow-down to Bl_Y S: over the centre Φ_B⁻¹ ∘ Φ_{S'} in the induced blow-up charts of one index over one induced flag chart, off the centre the unique point of Bl_Y S over π p.

Equations

• D.liftToBlowUp p = if hp : π ↑p ∈ Y then ↑(D.fChartB p hp).symm (↑(D.fChartS' p hp) p) else Exists.choose ⋯

theorem Manifold.RestrictBlowUpData.liftToBlowUp_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {p : ⋯.toAnalyticManifold.carrier} (hp : π ↑p ∈ Y) : D.liftToBlowUp p = ↑(D.fChartB p hp).symm (↑(D.fChartS' p hp) p)

theorem Manifold.RestrictBlowUpData.liftToBlowUp_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {p : ⋯.toAnalyticManifold.carrier} (hp : π ↑p ∉ Y) : D.liftToBlowUp p = Exists.choose ⋯

theorem Manifold.RestrictBlowUpData.proj_liftToBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) : D.proj (D.liftToBlowUp p) = D.blowDown p

The lift is over S.

theorem Manifold.RestrictBlowUpData.liftToBlowUp_eq_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {p : ⋯.toAnalyticManifold.carrier} (hp : π ↑p ∉ Y) {q : D.space.carrier} (hq : D.proj q = D.blowDown p) : D.liftToBlowUp p = q

Off the centre, the lift is the unique point off the divisor over π p.

theorem Manifold.RestrictBlowUpData.liftToBlowUp_eqOn_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {p : ⋯.toAnalyticManifold.carrier} (hp : π ↑p ∈ Y) : Set.EqOn D.liftToBlowUp (↑(D.fChartB p hp).symm ∘ ↑(D.fChartS' p hp)) (D.fChartS' p hp).source

Near a point over the centre, the lift is the chart formula Φ_B⁻¹ ∘ Φ_{S'}.

theorem Manifold.RestrictBlowUpData.exists_eqOn_liftToBlowUp_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {p : ⋯.toAnalyticManifold.carrier} (hp : π ↑p ∉ Y) : ∃ (N : Set ⋯.toAnalyticManifold.carrier), IsOpen N ∧ p ∈ N ∧ ∃ (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) D.space.carrier ⋯.toAnalyticManifold.carrier ⊤), N ⊆ ⇑D.blowDown ⁻¹' Ψ.target ∧ Set.EqOn D.liftToBlowUp (Ψ.invFun ∘ ⇑D.blowDown) N

Near a point off the centre, the lift is Ψ⁻¹ ∘ π|_{S'} for a local inverse Ψ of the blow-down of Bl_Y S.

theorem Manifold.RestrictBlowUpData.contMDiff_liftToBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : ContMDiff (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ D.liftToBlowUp

The lift S' → Bl_Y S is analytic.

The lift Bl_Y S → S'

noncomputable def Manifold.RestrictBlowUpData.liftFromBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) : ⋯.toAnalyticManifold.carrier

The lift of the blow-down of Bl_Y S to S': over the centre Φ_{S'}⁻¹ ∘ Φ_B in the induced blow-up charts of one index over one induced flag chart, off the centre the unique point of S' over the image.

Equations

• D.liftFromBlowUp q = if hq : ↑(D.proj q) ∈ Y then ↑(D.rChartS' q hq).symm (↑(D.rChartB q hq) q) else Exists.choose ⋯

theorem Manifold.RestrictBlowUpData.liftFromBlowUp_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {q : D.space.carrier} (hq : ↑(D.proj q) ∈ Y) : D.liftFromBlowUp q = ↑(D.rChartS' q hq).symm (↑(D.rChartB q hq) q)

theorem Manifold.RestrictBlowUpData.liftFromBlowUp_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {q : D.space.carrier} (hq : ↑(D.proj q) ∉ Y) : D.liftFromBlowUp q = Exists.choose ⋯

theorem Manifold.RestrictBlowUpData.blowDown_liftFromBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) : D.blowDown (D.liftFromBlowUp q) = D.proj q

The lift is over S.

theorem Manifold.RestrictBlowUpData.liftFromBlowUp_eq_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {q : D.space.carrier} (hq : ↑(D.proj q) ∉ Y) {p : ⋯.toAnalyticManifold.carrier} (hp : D.blowDown p = D.proj q) : D.liftFromBlowUp q = p

Off the centre, the lift is the unique point of S' off the divisor over the image.

theorem Manifold.RestrictBlowUpData.liftFromBlowUp_eqOn_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {q : D.space.carrier} (hq : ↑(D.proj q) ∈ Y) : Set.EqOn D.liftFromBlowUp (↑(D.rChartS' q hq).symm ∘ ↑(D.rChartB q hq)) (D.rChartB q hq).source

Near a point over the centre, the lift is the chart formula Φ_{S'}⁻¹ ∘ Φ_B.

theorem Manifold.RestrictBlowUpData.exists_eqOn_liftFromBlowUp_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) {q : D.space.carrier} (hq : ↑(D.proj q) ∉ Y) : ∃ (N : Set D.space.carrier), IsOpen N ∧ q ∈ N ∧ ∃ (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⋯.toAnalyticManifold.carrier ⋯.toAnalyticManifold.carrier ⊤), N ⊆ ⇑D.proj ⁻¹' Ψ.target ∧ Set.EqOn D.liftFromBlowUp (Ψ.invFun ∘ ⇑D.proj) N

Near a point off the centre, the lift is Ψ⁻¹ ∘ π_B for a local inverse Ψ of the restricted blow-down (Fields.lean).

theorem Manifold.RestrictBlowUpData.contMDiff_liftFromBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : ContMDiff (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ D.liftFromBlowUp

The lift Bl_Y S → S' is analytic.

The identification

theorem Manifold.RestrictBlowUpData.liftFromBlowUp_liftToBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (p : ⋯.toAnalyticManifold.carrier) : D.liftFromBlowUp (D.liftToBlowUp p) = p

The two lifts are inverse: S' → Bl_Y S → S'.

theorem Manifold.RestrictBlowUpData.liftToBlowUp_liftFromBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) (q : D.space.carrier) : D.liftToBlowUp (D.liftFromBlowUp q) = q

The two lifts are inverse: Bl_Y S → S' → Bl_Y S.

noncomputable def Manifold.RestrictBlowUpData.diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) D.space.carrier ⋯.toAnalyticManifold.carrier ⊤

The diffeomorphism Bl_Y S ≅ S' over S: Kollár's identification of Bl_{Z_i ∩ S_i} S_i with the birational transform of S_i [Kol07, Definition 30.2].

Equations

• D.diffeomorph = { toFun := D.liftFromBlowUp, invFun := D.liftToBlowUp, left_inv := ⋯, right_inv := ⋯, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem Manifold.RestrictBlowUpData.isBlowUp_blowDown {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (D : RestrictBlowUpData ψ π Y S c s) : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⋯.preimageVal Y) (c - s) ⇑D.blowDown

The restricted blow-down is a blowing-up of the bundled S along Y.

The two main statements

theorem Manifold.isBlowUp_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hYS : Y ⊆ S) : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.preimageVal Y) (c - s) ⇑(⋯.restrictMap hS π ⋯ ⋯)

The restricted blow-down π|_{S'} : S' → S is a blowing-up in the sense of [BM88, Definition 4.1] (IsBlowUp) of the bundled S along Y, of codimension c − s, in the induced charts: Kollár's S_{i+1} := Bl_{Z_i ∩ S_i} S_i, naturally identified with the birational transform of S_i [Kol07, Definition 30.2].

theorem Manifold.exists_diffeomorph_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {ψ : E ≃L[𝕜] Fin n → 𝕜} {π : M' → M} {Y S : Set M} {c s : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hYS : Y ⊆ S) : ∃ (g : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) ⋯).carrier ⋯.toAnalyticManifold.carrier ⊤), ∀ (p : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) ⋯).carrier), (⋯.restrictMap hS π ⋯ ⋯) (g p) = (blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) ⋯) p

The strict transform S' is identified over S with the blowing-up Bl_Y S [Kol07, Definition 30.2] (the identification is unique by IsBlowUp.exists_unique_diffeomorph).