Concatenation of sequences of centres

Step 2.1 of the proof of [Kol07, Theorem 103] applies Lemma 102 to each boundary member in turn, "at the end we get a blow-up sequence" Π : X_r → X: the blow-up sequences of the successive applications are composed, the value on the induced triple at the last stage being appended. This module defines the composition on sequences of centres, by recursion on the first sequence:

• BlowUpSequence.concat L L' — the sequence L followed by the sequence L' on the last stage of L (concat_nil, concat_cons, length_concat);
• noEmptyCenters_concat — the convention of no empty centres ([Kol07, 32]) is inherited from the pieces;
• isOfOrderGe_concat — the clauses (1′)–(4′) of [Kol07, Definition 66] hold for the concatenation when they hold for L starting with (𝓘, m, E) and for L' starting with the controlled transform and the boundary of L at its last stage.

The concatenation is the operation iterated in Step21Defs.lean.

def AnalyticManifold.BlowUpSequence.concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : BlowUpSequence ψ₀ (L.stage (Fin.last L.length)) → BlowUpSequence ψ₀ M

The concatenation of a sequence of centres L on M with a sequence L' on the last stage of L (the composition of blow-up sequences in Step 2.1 of the proof of [Kol07, Theorem 103]).

Equations

• (AnalyticManifold.BlowUpSequence.nil x✝).concat L' = L'
• (AnalyticManifold.BlowUpSequence.cons hY rest).concat L' = AnalyticManifold.BlowUpSequence.cons hY (rest.concat L')

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

theorem AnalyticManifold.BlowUpSequence.concat_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)) (L' : BlowUpSequence ψ₀ ((cons hY rest).stage (Fin.last (cons hY rest).length))) : (cons hY rest).concat L' = cons hY (rest.concat L')

theorem AnalyticManifold.BlowUpSequence.length_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) : (L.concat L').length = L.length + L'.length

The length of a concatenation is the sum of the lengths.

theorem AnalyticManifold.BlowUpSequence.noEmptyCenters_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) : L.NoEmptyCenters → L'.NoEmptyCenters → (L.concat L').NoEmptyCenters

A concatenation has no empty centre when the pieces have none ([Kol07, 32]).

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) {I E₀ : M.IdealSheaf} {m : ℕ} : L.toSuccession.IsOfOrderGe I m E₀ → L'.toSuccession.IsOfOrderGe (L.toSuccession.markedTransformSeq I m (Fin.last L.toSuccession.length)) m (L.toSuccession.boundarySeq E₀ (Fin.last L.toSuccession.length)) → (L.concat L').toSuccession.IsOfOrderGe I m E₀

The concatenation is a smooth blow-up sequence of order ≥ m starting with (𝓘, m, E₀) ([Kol07, Definition 66 (1′)–(4′)]) when L is, and L' is one starting with the controlled transform and the boundary of L at its last stage.