Step 2 on an open is of order ≥ s for the full transformed boundary

The triple of Step 2.2 carries the boundary E^{exc}_r + H_r of exceptional divisors and the transform of the hypersurface of maximal contact, while the clause of [Kol07, Definition 66] for Step 2 as a whole concerns the full transformed boundary, which also contains the transforms of the original members E^j. After Step 2.1 these miss the cosupport {ord I_r ≥ s} (the conclusion of [Kol07, 104, Step 2.1.j]: "Π^{-1}_{r(s)∗} E is disjoint from cosupp(I_{r(s)}, m)"), so a member of the full boundary through the cosupport is an exceptional divisor, a member of both boundaries; this is what lets the order clause pass from the one boundary to the other.

• BO.fullToPosIdxOf, BO.exists_exceptionalEmb_of_mem_of_disjoint, BO.isOfOrderGe_full_of_positional — over an arbitrary sequence L of order ≥ s: a correspondence from the members of the full boundary to those of E^{exc}_r + H_r sending an exceptional divisor to itself; a member of the full boundary through the cosupport is an exceptional divisor when the transforms of the original members miss the cosupport; and a sequence of order ≥ s for the triple of Step 2.2 restricted to an open is then of order ≥ s for the induced triple (Induced.lean) restricted to the open.
• BO.hfStep22FamOn_isOfOrderGe_positional, BO.hfStep22FamOn_isOfOrderGe_full — the value of Step 2.2 on its reading open is of order ≥ s for the restricted triple of Step 2.2 (the order clause of the data at the re-tuned mark, carried back through the tuning by orderReduction_tuned_iff), hence for the restricted induced triple (the cosupport clause of the chain of Step 2.1, Step21FamCosupp.lean).
• hfStep2SeqFamOn_isOfOrderGe — the value of Step 2 on U is a smooth blow-up sequence of order ≥ s starting with the restricted triple (U, 𝓘|_U, E|_U): the appended chain is of order ≥ s (isOfOrderGe_shrinkAppend), then restricted to U and its empty blow-ups deleted.

The hf… declarations are the general forms over data d : HFData ψ₀ s of Step 2 (HFamData.lean); the plain forms are their instances at Lemma 102's data. This is the order clause of the family structure BOanFam for the local functor (LocalFunctorFam.lean).

noncomputable def Hironaka.Manifold.BO.fullToPosIdxOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) : (T.induced s L hL).F.ι → (step22TripleOf T L hL hsnc).F.ι

A correspondence from the members of the full transformed boundary (the induced triple) to those of the boundary E^{exc}_r + H_r of the triple of Step 2.2: an exceptional divisor to itself (chosen among the members indexing that divisor), the transform of an original member to an arbitrary member. Only the values at exceptional divisors matter.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BO.fullToPosIdxOf_spec {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (a : (T.induced s L hL).F.ι) (hk : ∃ (k : (L.toSuccession.totalTransformSeqAux ↑(Fin.last L.toSuccession.length) ⋯).ι), a = L.toSuccession.exceptionalEmb T.F ↑(Fin.last L.toSuccession.length) ⋯ k) : ∃ (k : (L.toSuccession.totalTransformSeqAux ↑(Fin.last L.toSuccession.length) ⋯).ι), a = L.toSuccession.exceptionalEmb T.F ↑(Fin.last L.toSuccession.length) ⋯ k ∧ fullToPosIdxOf T L hL hsnc a = toLex (Sum.inl k)

At an exceptional divisor E_k, the correspondence picks a member indexing that divisor.

theorem Hironaka.Manifold.BO.exists_exceptionalEmb_of_mem_of_disjoint {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hdis : ∀ (j : T.F.ι), Disjoint {x : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq T.I s (Fin.last L.toSuccession.length)) x} (L.toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last L.toSuccession.length))) (a : (T.induced s L hL).F.ι) (ha : ∃ x ∈ (T.induced s L hL).F.hyp a, ↑s ≤ Manifold.IdealSheaf.ord (T.induced s L hL).I x) : ∃ (k : (L.toSuccession.totalTransformSeqAux ↑(Fin.last L.toSuccession.length) ⋯).ι), a = L.toSuccession.exceptionalEmb T.F ↑(Fin.last L.toSuccession.length) ⋯ k

A member of the full transformed boundary meeting the cosupport {ord I_r ≥ s} is an exceptional divisor, when the transforms of the original members miss the cosupport (the conclusion of Step 2.1, [Kol07, 104, Step 2.1.j]).

theorem Hironaka.Manifold.BO.isOfOrderGe_full_of_positional {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (hdis : ∀ (j : T.F.ι), Disjoint {x : ↑↧(L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier | ↑s ≤ Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq T.I s (Fin.last L.toSuccession.length)) x} (L.toSuccession.strictTransformSeq (T.F.hyp j) (Fin.last L.toSuccession.length))) (O : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) (S : AnalyticManifold.BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict O)) (hpos : S.toSuccession.IsOfOrderGe ((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).I s ((step22TripleOf T L hL hsnc).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.idealSheaf) : S.toSuccession.IsOfOrderGe ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).I s ((T.induced s L hL).pullback ((L.stage (Fin.last L.length)).inclusion O) ⋯).F.idealSheaf

Over an arbitrary sequence L of order ≥ s and restricted to an open O of its last stage: a sequence of order ≥ s for the restricted triple of Step 2.2 (boundary E^{exc}_r + H_r) is of order ≥ s for the restricted induced triple (the full transformed boundary), provided the transforms of the original members miss the cosupport. The members of the full boundary through the cosupport are exceptional divisors (exists_exceptionalEmb_of_mem_of_disjoint, the order read at the point's image in the last stage), members of both boundaries, so the normal-crossings condition on the centres transfers (IsOfOrderGe.of_forall_hyp_eq_of_mem).

theorem Hironaka.Manifold.BO.hfStep22FamOn_isOfOrderGe_positional {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) : (hfStep22FamOn T s d hT U hU hH hle).toSuccession.IsOfOrderGe ((hfStep22TripleFam T s d hT U hU hH hle).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).I s ((hfStep22TripleFam T s d hT U hU hH hle).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).F.idealSheaf

The value of Step 2.2 on its reading open is of order ≥ s for the triple of Step 2.2 restricted to the open (over data d): the order clause of the data at the re-tuned mark, the tuned triple pulled back being the pulled-back triple tuned (tuned_pullback), carried back through the tuning by orderReduction_tuned_iff.

theorem Hironaka.Manifold.BO.hfStep22FamOn_isOfOrderGe_full {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) : (hfStep22FamOn T s d hT U hU hH hle).toSuccession.IsOfOrderGe (((T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).induced s (hfStep2FamChain T s d hT U hU).L ⋯).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).I s (((T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).induced s (hfStep2FamChain T s d hT U hU).L ⋯).pullback (((hfStep2FamChain T s d hT U hU).L.stage (Fin.last (hfStep2FamChain T s d hT U hU).L.length)).inclusion (hfStep2ReadOpen T s d hT U hU)) ⋯).F.idealSheaf

The value of Step 2.2 on its reading open is of order ≥ s for the restricted induced triple, with the full transformed boundary (over data d): the clause for the boundary E^{exc}_r + H_r (hfStep22FamOn_isOfOrderGe_positional) and the cosupport clause of the chain of Step 2.1 for every original member (step21FamAux_cosupp_disjoint; an empty member has empty strict transform), through isOfOrderGe_full_of_positional.

theorem Hironaka.Manifold.hfStep2SeqFamOn_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) : (BO.hfStep2SeqFamOn T s d hT U hU hH hle).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The value of Step 2 on the open U is a smooth blow-up sequence of order ≥ s starting with the restricted triple (U, 𝓘|_U, E|_U), with the full boundary (Kol07, Definition 66 (1′)–(4′); over data d): the chain of Step 2.1 with the value of Step 2.2 appended is of order ≥ s for the triple restricted to the next open (isOfOrderGe_shrinkAppend with hfStep22FamOn_isOfOrderGe_full), then restricted to U (isOfOrderGe_pullback) and its empty blow-ups deleted (isOfOrderGe_eraseEmpty).