Lemma 102: the order clause and clause (1), unconditionally

The order clause of [Kol07, Lemma 102] (BDCore.lean) and its clause (1) (BDCosupp.lean) were proved for the construction BDan under the hypothesis PushforwardBridge ψ₀: the push-forward of a list of centres without empty centres on a closed hypersurface has, as succession of blow-ups, the push-forward of the succession of the list ([Kol07, 30.3]). This identification is BlowUpSequence.toSuccession_pushforward (Hironaka/Manifold/FiniteSuccession/Functor/ToSuccessionPushforward.lean), so both clauses hold outright.

• pushforwardBridge ψ — the identification for every model.
• BDan_isOfOrder, BDan_cosupp_disjoint — the two clauses of Lemma 102 for BDan.

theorem Hironaka.Manifold.pushforwardBridge {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) : PushforwardBridge ψ

The push-forward of a list of centres without empty centres along a closed hypersurface has, as succession of blow-ups, the push-forward of the succession of the list: BlowUpSequence.toSuccession_pushforward at codimension one.

theorem Hironaka.Manifold.BDan_isOfOrder {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) : (BDan m inp T hT j).toSuccession.IsOfOrder T.I T.F.idealSheaf m

BD_{n,m,j}(M, 𝓘, E) is a smooth blow-up sequence of order m starting with (M, 𝓘, E) ([Kol07, Lemma 102]; the going-up statement [Kol07, Corollary 85] for the tail): the order clause BDan_isOfOrder_of_bridge with the identification of the two push-forwards supplied.

theorem Hironaka.Manifold.BDan_cosupp_disjoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) : Disjoint {x : ↑↧((BDan m inp T hT j).toSuccession.stage (Fin.last (BDan m inp T hT j).toSuccession.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord ((BDan m inp T hT j).toSuccession.weakTransformSeq T.I (Fin.last (BDan m inp T hT j).toSuccession.length)) x} ((BDan m inp T hT j).toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last (BDan m inp T hT j).toSuccession.length))

The birational transform of E^j at the end of BD_{n,m,j}(M, 𝓘, E) misses the cosupport {ord I_r ≥ m} ([Kol07, Lemma 102 (1)]): BDan_cosupp_disjoint_of_bridge with the identification of the two push-forwards supplied.