The clauses of eraseEmpty and map on lists of centres

The recursion BlowUpSequence.eraseEmpty (Hironaka.Manifold.FiniteSuccession.Functor.EraseEmpty) deletes the empty steps of a list of centres and carries the tails back along the analytic isomorphisms Bl_∅ M ≃ M; here are its clauses: the equations on nil and cons (eraseEmpty_nil, eraseEmpty_cons_of_ne_empty, eraseEmpty_cons_empty); the transport map keeps the length and the (non-)emptiness of the centres (length_map, noEmptyCenters_map_iff); the cleaned list has no empty centre (noEmptyCenters_eraseEmpty); the deletion is the identity exactly on lists without empty centres (eraseEmpty_eq_self_iff) and is idempotent (eraseEmpty_eraseEmpty); a functor's outputs are fixed by it (eraseEmpty_seq, the convention of [Kol07, 32]). A functor is its assignment of lists (AnalyticBlowUpSequenceAssignment.ext).

theorem Manifold.AnalyticBlowUpSequenceAssignment.ext {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {B B' : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} (h : ∀ {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (hT : Dom T), B.seq T hT = B'.seq T hT) : B = B'

A functor is its assignment of lists of centres (the other field is a proof).

The equations of eraseEmpty

@[simp]

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

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_cons {𝕜 : 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)) : (cons hY rest).eraseEmpty = eraseEmptyCons hY rest.eraseEmpty

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_cons_of_ne_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) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (hne : Y ≠ ∅) : (cons hY rest).eraseEmpty = cons hY rest.eraseEmpty

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_cons_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) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (hY₀ : Y = ∅) : (cons hY rest).eraseEmpty = map (emptyBlowUpDiffeomorph hY hY₀) rest.eraseEmpty

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_cons_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) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (hY₀ : Y = ∅) : ∃ (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (Manifold.blowUp ψ₀ hY).carrier M.carrier ⊤), (∀ (p : (Manifold.blowUp ψ₀ hY).carrier), g p = (Manifold.blowUpπ ψ₀ hY) p) ∧ (cons hY rest).eraseEmpty = map g rest.eraseEmpty

Lengths and empty centres

theorem AnalyticManifold.BlowUpSequence.length_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} : (nil M).length = 0

theorem AnalyticManifold.BlowUpSequence.length_cons {𝕜 : 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)) : (cons hY rest).length = rest.length + 1

theorem AnalyticManifold.BlowUpSequence.length_map {𝕜 : 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 ⊤) (L : BlowUpSequence ψ₀ M) : (map g L).length = L.length

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

No empty centre in nil.

theorem AnalyticManifold.FiniteSuccession.isEmptyAt_cons_zero {𝕜 : 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) (R : (Manifold.blowUp ψ₀ hY).FiniteSuccession) : (cons ψ₀ hY R).IsEmptyAt 0 ↔ Y = ∅

The first centre of the succession cons hY R is empty iff Y = ∅ (isEmptyAt_iff with cosupport_idealSheaf).

theorem AnalyticManifold.FiniteSuccession.isEmptyAt_cons_succ {𝕜 : 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) (R : (Manifold.blowUp ψ₀ hY).FiniteSuccession) (i : Fin R.length) : (cons ψ₀ hY R).IsEmptyAt i.succ ↔ R.IsEmptyAt i

The later centres of cons hY R are those of R.

@[simp]

theorem AnalyticManifold.BlowUpSequence.noEmptyCenters_cons_iff {𝕜 : 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)) : (cons hY rest).NoEmptyCenters ↔ Y ≠ ∅ ∧ rest.NoEmptyCenters

cons hY rest has no empty centre iff Y ≠ ∅ and rest has none.

theorem AnalyticManifold.BlowUpSequence.noEmptyCenters_map_iff {𝕜 : 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 ⊤) (L : BlowUpSequence ψ₀ M) : (map g L).NoEmptyCenters ↔ L.NoEmptyCenters

The transport along an analytic isomorphism keeps the (non-)emptiness of every centre.

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

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

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_eq_self_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : L.eraseEmpty = L ↔ L.NoEmptyCenters

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

theorem Manifold.AnalyticBlowUpSequenceAssignment.eraseEmpty_seq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} (B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom) {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (hT : Dom T) : (B.seq T hT).eraseEmpty = B.seq T hT

[Kol07, 32]: deleting empty blow-ups from an output of a functor changes nothing.