Blow-up sequences as lists of centres

A blow-up sequence is determined by its list of centres [Kol07, Definition 29]. This module realises that view on analytic manifolds: the inductive type CenterList ψ₀ M of blow-up sequences (X_r, …) → ⋯ → (X_0) = M given by their centres, with constructors nil M and cons hY rest, where hY : IsClosedSubmanifold ψ₀ Y c is a closed submanifold of the current stage and rest a list on the blowing-up blowUp ψ₀ hY, with one fixed model chart ψ₀ : E ≃L[𝕜] (Fin n → 𝕜) for every stage. The algebraic counterpart is the inductive BlowUpSequence X, on which equality is equality of the centres, the form in which the uniqueness theorem for blow-up sequence functors [Kol07, Theorem 97] concludes B = B'. On the structure FiniteSuccession M (Włodarczyk's finite sequence, with the stages, blow-downs and chart data as fields) equality is strictly finer than equality of the centres, since a stage may be replaced by a diffeomorphic copy and the chart of a stage is chosen from isMonoidal i; the uniqueness theorems for analytic blow-up sequences are therefore stated on lists. Every list is a FiniteSuccession through toSuccession (the constructors FiniteSuccession.nil and FiniteSuccession.cons), so that the theorems on sequences apply to it.

• CenterList ψ₀ M, toSuccession, length, stage;
• pullback L h hh: the pull-back h^*B of the list along a local analytic isomorphism h : N → M [Kol07, 30.1], with the blowing-up of the preimage centre in place of the fibre product X_{i+1} ×_X Y: by recursion on the list, the centre h_i⁻¹(Z_i) at every stage (IsClosedSubmanifold.preimage_of_isLocalDiffeomorph) and the lift h_{i+1} of h_i to the blow-ups (blowUpLift, liftStep), canonically and with no choice of chart;
• pullbackLift L h hh i: the lifts h_i : N_i → M_i, local analytic isomorphisms;
• length_pullback, toSuccession_nil, toSuccession_cons, pullback_nil, pullback_cons, and the recursion stageMapAux_cons_succ of the composite blow-down.

inductive AnalyticManifold.BlowUpSequence {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) : AnalyticManifold 𝕜 E → Type (max (u + 1) v)

A blow-up sequence as its list of centres [Kol07, Definition 29], on analytic manifolds: nil M is the empty sequence, and cons hY rest blows up the closed submanifold Y of the current stage (hY : IsClosedSubmanifold ψ₀ Y c, with the model chart ψ₀ fixed once for all stages) and continues with rest on the blowing-up blowUp ψ₀ hY. Equality of lists is equality of the centres stage by stage (the hY fields are proofs).

• nil {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (M : AnalyticManifold 𝕜 E) : BlowUpSequence ψ₀ M
• cons {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) : BlowUpSequence ψ₀ M

def AnalyticManifold.BlowUpSequence.toSuccession {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} : BlowUpSequence ψ₀ M → M.FiniteSuccession

The list as a finite sequence of monoidal transformations (through the constructors nil and cons of FiniteSuccession), so that every theorem on sequences applies to it.

Equations

• (AnalyticManifold.BlowUpSequence.nil x✝).toSuccession = AnalyticManifold.FiniteSuccession.nil x✝
• (AnalyticManifold.BlowUpSequence.cons hY rest).toSuccession = AnalyticManifold.FiniteSuccession.cons ψ₀ hY rest.toSuccession

theorem AnalyticManifold.BlowUpSequence.toSuccession_nil {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (M : AnalyticManifold 𝕜 E) : (nil M).toSuccession = FiniteSuccession.nil M

@[simp]

theorem AnalyticManifold.BlowUpSequence.toSuccession_cons {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) : (cons hY rest).toSuccession = FiniteSuccession.cons ψ₀ hY rest.toSuccession

@[reducible, inline]

noncomputable abbrev AnalyticManifold.BlowUpSequence.length {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : ℕ

The length r (the number of blow-ups).

Equations

• L.length = L.toSuccession.length

@[reducible, inline]

noncomputable abbrev AnalyticManifold.BlowUpSequence.stage {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (i : Fin (L.length + 1)) : AnalyticManifold 𝕜 E

The stages M = M_0, M_1, …, M_r.

Equations

• L.stage i = L.toSuccession.stage i

The pull-back along a local analytic isomorphism

noncomputable def AnalyticManifold.BlowUpSequence.liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) : AnalyticMap (Manifold.blowUp ψ₀ ⋯) (Manifold.blowUp ψ₀ hY)

One step of the pull-back: the lift h₁ : Bl_{h⁻¹Y} N → Bl_Y M of the local analytic isomorphism h over the two blow-downs, as a bundled analytic map.

Equations

• AnalyticManifold.BlowUpSequence.liftStep h hh hY = ⟨Manifold.blowUpLift hY hh ⋯ ⋯, ⋯⟩

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(liftStep h hh hY)

The lift is a local analytic isomorphism (isLocalDiffeomorph_blowUpLift).

theorem AnalyticManifold.BlowUpSequence.blowUpπ_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (q : (Manifold.blowUp ψ₀ ⋯).carrier) : (Manifold.blowUpπ ψ₀ hY) ((liftStep h hh hY) q) = h ((Manifold.blowUpπ ψ₀ ⋯) q)

The lift lies over h: π ∘ h₁ = h ∘ π'.

def AnalyticManifold.BlowUpSequence.pullback {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} : BlowUpSequence ψ₀ M → (h : AnalyticMap N M) → IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h → BlowUpSequence ψ₀ N

The pull-back h^*L of the list along a local analytic isomorphism h : N → M [Kol07, 30.1]: the list of the preimage centres h_i⁻¹(Z_i) under the successive lifts h_i, by recursion on the list.

Equations

• (AnalyticManifold.BlowUpSequence.nil x).pullback x_2 x_3 = AnalyticManifold.BlowUpSequence.nil x_1
• (AnalyticManifold.BlowUpSequence.cons hY rest).pullback x_2 x_3 = AnalyticManifold.BlowUpSequence.cons ⋯ (rest.pullback (AnalyticManifold.BlowUpSequence.liftStep x_2 x_3 hY) ⋯)

@[simp]

theorem AnalyticManifold.BlowUpSequence.pullback_nil {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (nil M).pullback h hh = nil N

@[simp]

theorem AnalyticManifold.BlowUpSequence.pullback_cons {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (cons hY rest).pullback h hh = cons ⋯ (rest.pullback (liftStep h hh hY) ⋯)

@[simp]

theorem AnalyticManifold.BlowUpSequence.length_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (L.pullback h hh).length = L.length

The pull-back has the length of the list.

def AnalyticManifold.BlowUpSequence.pullbackLiftAux {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1) : AnalyticMap (N.finStages (L.pullback h hh).toSuccession.later ⟨i, hi'⟩) (M.finStages L.toSuccession.later ⟨i, hi⟩)

The lifts h_i : N_i → M_i of h to the stages of the pull-back, indexed by the stage number (h_0 = h, h_{i+1} the lift of h_i, liftStep).

Equations

• (AnalyticManifold.BlowUpSequence.nil x).pullbackLiftAux x_2 x_3 0 x_11 x_12 = x_2
• (AnalyticManifold.BlowUpSequence.cons hY rest).pullbackLiftAux x_2 x_3 0 x_11 x_12 = x_2
• (AnalyticManifold.BlowUpSequence.cons hY rest).pullbackLiftAux x_2 x_3 i.succ hi hi' = rest.pullbackLiftAux (AnalyticManifold.BlowUpSequence.liftStep x_2 x_3 hY) ⋯ i ⋯ ⋯
• (AnalyticManifold.BlowUpSequence.nil x).pullbackLiftAux x_2 x_3 i.succ hi x_12 = absurd hi ⋯

noncomputable def AnalyticManifold.BlowUpSequence.pullbackLift {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (i : Fin (L.length + 1)) : AnalyticMap ((L.pullback h hh).stage ⟨↑i, ⋯⟩) (L.stage i)

The lifts h_i : N_i → M_i of the local analytic isomorphism h to the stages of h^*L and L.

Equations

• L.pullbackLift h hh i = L.pullbackLiftAux h hh ↑i ⋯ ⋯

theorem AnalyticManifold.BlowUpSequence.pullbackLift_zero {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : L.pullbackLift h hh 0 = h

theorem AnalyticManifold.BlowUpSequence.stageMapAux_cons_succ {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (i : ℕ) (hi : i + 1 < (cons hY rest).toSuccession.length + 1) (p : ((cons hY rest).toSuccession.stage ⟨i + 1, hi⟩).carrier) : ((cons hY rest).toSuccession.stageMapAux (i + 1) hi) p = (Manifold.blowUpπ ψ₀ hY) ((rest.toSuccession.stageMapAux i ⋯) p)

The composite blow-down of the list cons hY rest at stage i + 1 is the first blow-down after the composite of the rest at stage i.