Transport of a list of centres along an analytic isomorphism, and the deletion of empty blow-ups

Kollár adopts the convention that the final outputs of the named blow-up sequence functors do not contain empty blow-ups; the steps of their construction that happen to lead to empty blow-ups "are then ignored without explicit mention" [Kol07, 32]. Accordingly B(Y, h^* I, h⁻¹(E)) is obtained from the pull-back h^* B(X, I, E) by deleting every blow-up h^* π_i whose centre is empty and reindexing [Kol07, 34.1]. The definition of the deletion needs the fact that a blowing-up composed with an analytic isomorphism of its base is a blowing-up with the transported centre (IsBlowUp.diffeomorph_comp).

On the lists of centres CenterList ψ₀ M:

• BlowUpSequence.liftDiffeomorph g hY: the lift Bl_Y M ≃ Bl_{g(Y)} N of an analytic isomorphism g : M ≃ N to the chosen blowings-up, the canonical isomorphism (IsBlowUp.exists_unique_diffeomorph) between g ∘ π_Y (a blowing-up of N along g(Y), IsBlowUp.diffeomorph_comp) and π_{g(Y)};
• BlowUpSequence.map g L: the list transported along g: the centres g(Y_i) (IsClosedSubmanifold.image_diffeomorph), the tails along the lifts;
• BlowUpSequence.emptyBlowUpDiffeomorph hY hY₀: the analytic isomorphism Bl_∅ M ≃ M of an empty blowing-up (IsBlowUp.exists_diffeomorph_of_empty; the empty blow-up of [Kol07, Warning 20]), whose map is π itself (∀ p, g p = π p), so that the choice is only of the proof-carrying wrapper of a determined function; the analogue for schemes is the inverse of the blow-down of the empty blow-up used by Scheme.BlowUpSequence.eraseEmpty;
• BlowUpSequence.eraseEmpty L: delete every empty blow-up and reindex, by recursion on the list: the empty step cons h∅ rest is removed by carrying rest.eraseEmpty, a list on Bl_∅ M, back to M along that isomorphism (the analogue of the scheme-theoretic Scheme.BlowUpSequence.eraseEmpty);
• BlowUpSequence.NoEmptyCenters L: no centre is empty (the NoEmptyCenters of the succession).

@[reducible, inline]

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

[Kol07, 32] on lists: no centre of the list is empty — NoEmptyCenters of the succession.

Equations

• L.NoEmptyCenters = L.toSuccession.NoEmptyCenters

noncomputable def AnalyticManifold.BlowUpSequence.liftDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (Manifold.blowUp ψ₀ hY).carrier (Manifold.blowUp ψ₀ ⋯).carrier ⊤

The lift Bl_Y M ≃ Bl_{g(Y)} N of an analytic isomorphism g : M ≃ N to the chosen blowings-up: canonical isomorphism between g ∘ π_Y, a blowing-up of N along g(Y) (IsBlowUp.diffeomorph_comp), and the chosen blowing-up π_{g(Y)}.

Equations

• AnalyticManifold.BlowUpSequence.liftDiffeomorph g hY = Manifold.IsBlowUp.diffeomorph ⋯ ⋯ ⋯

def AnalyticManifold.BlowUpSequence.map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤ → BlowUpSequence ψ₀ M → BlowUpSequence ψ₀ N

The list of centres transported along an analytic isomorphism g : M ≃ N: the centres g(Y_i) (IsClosedSubmanifold.image_diffeomorph), the tails along the lifts liftDiffeomorph.

Equations

• One or more equations did not get rendered due to their size.
• AnalyticManifold.BlowUpSequence.map x✝ (AnalyticManifold.BlowUpSequence.nil x✝²) = AnalyticManifold.BlowUpSequence.nil x✝¹

theorem AnalyticManifold.BlowUpSequence.map_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) : map g (nil M) = nil N

theorem AnalyticManifold.BlowUpSequence.map_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) : map g (cons hY rest) = cons ⋯ (map (liftDiffeomorph g hY) rest)

theorem AnalyticManifold.BlowUpSequence.isBlowUp_blowUpπ_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) : Manifold.IsBlowUp ψ₀ ∅ c ⇑(Manifold.blowUpπ ψ₀ hY)

The chosen blowing-up along an empty centre, read as a blowing-up along ∅.

noncomputable def AnalyticManifold.BlowUpSequence.emptyBlowUpDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (Manifold.blowUp ψ₀ hY).carrier M.carrier ⊤

[Kol07, Warning 20] ("π_{Z,X} is an isomorphism" for Z = ∅): the analytic isomorphism Bl_∅ M ≃ M of an empty blowing-up — the one whose map is π itself (emptyBlowUpDiffeomorph_apply); the choice is of the proof-carrying wrapper of a determined function.

Equations

• AnalyticManifold.BlowUpSequence.emptyBlowUpDiffeomorph hY hY₀ = Classical.choose ⋯

theorem AnalyticManifold.BlowUpSequence.emptyBlowUpDiffeomorph_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) (p : (Manifold.blowUp ψ₀ hY).carrier) : (emptyBlowUpDiffeomorph hY hY₀) p = (Manifold.blowUpπ ψ₀ hY) p

noncomputable def AnalyticManifold.BlowUpSequence.eraseEmptyCons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [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

One step of eraseEmpty: the step cons hY rest with the tail already cleaned — dropped (the tail carried back along Bl_∅ M ≃ M) when Y = ∅, kept otherwise.

Equations

• One or more equations did not get rendered due to their size.

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

[Kol07, 32] and 34.1: delete every empty blow-up and reindex — by recursion on the list, an empty step cons h∅ rest is removed by carrying the cleaned tail, a list on Bl_∅ M, back to M along the analytic isomorphism Bl_∅ M ≃ M of the empty blowing-up (the scheme-theoretic eraseEmpty with pullback (inv (blowUpπ X ⊤))).

Equations

• (AnalyticManifold.BlowUpSequence.nil x✝).eraseEmpty = AnalyticManifold.BlowUpSequence.nil x✝
• (AnalyticManifold.BlowUpSequence.cons hY rest).eraseEmpty = AnalyticManifold.BlowUpSequence.eraseEmptyCons hY rest.eraseEmpty