Clauses along a concatenation of lists of centres

The value of the principalization functor on an open is a concatenation (BlowUpSequence.concat): the disjoining list of [Kol07, 72] followed by the order-reduction list on the disjoined triple. Two clauses of the value are read stage by stage and pass through the concatenation by induction on the first list:

• clause (3′) of [Kol07, Definition 66] — the boundary E_i (boundarySeq) has only normal crossings with the centre Z_i — holds along L.concat L' when it holds along L and along L' started from L's last boundary (hasOnlyNormalCrossingsWith_boundarySeq_concat; the boundary along cons hY rest after the first step is the boundary along rest from the reduced transform, cons_boundarySeq_succ);
• the centres of L.concat L' lie over Z when those of L do and those of L' lie over the preimage of Z under L's composite (centersOver_concat; the composite of cons hY rest after the first step factors through the first blow-down, stageMapAux_cons_succ).

The boundary at a stage of the concatenation is not stated as an equation (its two sides live on the two lists' stage types, equal only propositionally); the clauses are transported instead. These are the two facts behind clauses (1) and (3) of [Kol07, Theorem 35] for the value (ClauseOne.lean, ClauseThree.lean).

theorem AnalyticManifold.BlowUpSequence.hasOnlyNormalCrossingsWith_boundarySeq_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))) (E₀ : M.IdealSheaf) : (∀ (i : Fin L.toSuccession.length), (L.toSuccession.boundarySeq E₀ i.castSucc).HasOnlyNormalCrossingsWith (L.toSuccession.center i)) → (∀ (i : Fin L'.toSuccession.length), (L'.toSuccession.boundarySeq (L.toSuccession.boundarySeq E₀ (Fin.last L.toSuccession.length)) i.castSucc).HasOnlyNormalCrossingsWith (L'.toSuccession.center i)) → ∀ (i : Fin (L.concat L').toSuccession.length), ((L.concat L').toSuccession.boundarySeq E₀ i.castSucc).HasOnlyNormalCrossingsWith ((L.concat L').toSuccession.center i)

Clause (3′) of [Kol07, Definition 66] along a concatenation: if every centre of L has only normal crossings with the boundary from E₀ at its stage, and every centre of L' has only normal crossings with the boundary from L's last boundary at its stage, then every centre of L.concat L' has only normal crossings with the boundary from E₀ at its stage.

theorem AnalyticManifold.BlowUpSequence.centersOver_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))) (Z : Set M.carrier) : L.toSuccession.CentersOver Z → L'.toSuccession.CentersOver (⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' Z) → (L.concat L').toSuccession.CentersOver Z

The centres of a concatenation lie over Z when those of the first list do and those of the second list lie over the preimage of Z under the first list's composite.