Step 2: the order drop along a concatenation #
Step 2.2 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.2]): at the end the cosupport
of the controlled transform of (I, m) misses the transform of H while, H being a
hypersurface of maximal contact, it lies in that transform, so it is empty. The order drop at the
end of Step 2.2 gives that at the end of the whole of Step 2 by the concatenation.
BlowUpSequence.forall_ord_lt_concat_of_forall— the order drop along a concatenation.
The order drop for Step 2 on a relatively compact open is proved in Step22FamOrdLt.lean.
theorem
AnalyticManifold.BlowUpSequence.forall_ord_lt_concat_of_forall
{𝕜 : 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 : M.IdealSheaf)
(s : ℕ)
:
(∀ (x : ↑↧(L'.toSuccession.stage (Fin.last L'.toSuccession.length)).carrier),
Manifold.IdealSheaf.ord
(L'.toSuccession.weakTransformSeq (L.toSuccession.weakTransformSeq I (Fin.last L.toSuccession.length))
(Fin.last L'.toSuccession.length))
x < ↑s) →
∀ (x : ↑↧((L.concat L').toSuccession.stage (Fin.last (L.concat L').toSuccession.length)).carrier),
Manifold.IdealSheaf.ord ((L.concat L').toSuccession.weakTransformSeq I (Fin.last (L.concat L').toSuccession.length))
x < ↑s
The order drop at the last stage of a concatenation L.concat L' follows from the order drop at
the last stage of L' for the weak transform reached by L; by induction on L, reading through
the first blow-up (cons_weakTransformSeq_succ).