The rounds of order reduction along a shrinking chain: the resolution family

Hironaka's Main Theorem II(N) [Hir64, p. 176] iterates order reduction with the maximal order d = max ord decreasing: run the order reduction of (𝓘, d) at the maximal order d, then again on the weak transform (whose order is < d), down to d = 1. Here each round is the value of the order-reduction family BO_{n,d} of [Kol07, Theorem 68] (BOanFam 𝕜 n d, the binder bo d) on the current derived triple, a CompatibleFamily whose sequences exist only on relatively compact opens; so the rounds are read along a shrinking chain of relatively compact opens: round d + 1 is read at Ω d, the derived triple is the induced triple at mark d + 1 (AnalyticTriple.induced, in the class of BO_{n,d} by the round's ord_lt), the chain is lifted to the round's last stage as the preimages under the proper composite blow-down, and the rounds from d are concatenated after the round's list pulled back to the open whose value is wanted. The recursion is one recursion on d over the current manifold (resolveFrom): the concatenation's second factor lives on the first factor's last stage by construction, so no stage transport is needed. The value on a relatively compact open U (resolveSeqOn) is the recursion along the canonical chain, d_U + 1 iterated shrinks of closure U inside the open {ord 𝓘 ≤ d_U} (upper semicontinuity of the order, isOpen_setOf_ord_le; d_U the least bound of ord 𝓘 on closure U, bddAbove_ord_on_compact), so that the triple restricted to the outermost open lies in the class of BO_{n,d_U} when d_U ≥ 1 (boClass_pullback_inclusion), with the empty blow-ups erased (the empty blow-up convention [Kol07, 32]). The opens of a fixed exhaustion alone would make the round count circular (the bound on the outermost open depends on the open chosen); the rounds above the order bound of an open are empty on it (the remark after [Kol07, Theorem 68]), which enters canonicity (Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean), not the definition. The value along an arbitrary admissible chain (ResolveChain, resolveSeqOnAlong) is what canonicity compares.

This is Włodarczyk's locally finite principalization [Wlo09, Theorem 2.0.3 (1)], with the neighbourhoods U of the compact sets read as relatively compact opens, and the reduction of the maximal order of [Wlo09, §6, Step 2a]; Bierstone and Milman treat the non-compact case by relatively compact opens (the remark after [BM97, Theorem 1.6]). Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean proves that the value does not depend on the chain and bundles the values into resolveFam.

Shrinking a compact inside an open (the chain's opens)

theorem Hironaka.Manifold.locallyCompactSpace_std {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) : LocallyCompactSpace M.carrier

A manifold modelled on 𝕜ⁿ is locally compact.

theorem Hironaka.Manifold.exists_shrinkBetween {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : ∃ (W : TopologicalSpace.Opens M.carrier), K ⊆ ↑W ∧ closure ↑W ⊆ ↑V ∧ IsCompact (closure ↑W)

Between a compact K and an open V ⊇ K there is a relatively compact open W with K ⊆ W and closure W ⊆ V (Mathlib's exists_open_between_and_isCompact_closure, the manifold being locally compact and Hausdorff, hence regular).

noncomputable def Hironaka.Manifold.shrinkBetween {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K : Set M.carrier) (V : TopologicalSpace.Opens M.carrier) (hK : IsCompact K) (hKV : K ⊆ ↑V) : TopologicalSpace.Opens M.carrier

A chosen open between a compact and an open containing it (Classical.choose of exists_shrinkBetween).

Equations

• Hironaka.Manifold.shrinkBetween K V hK hKV = Classical.choose ⋯

theorem Hironaka.Manifold.subset_shrinkBetween {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : K ⊆ ↑(shrinkBetween K V hK hKV)

theorem Hironaka.Manifold.closure_shrinkBetween_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : closure ↑(shrinkBetween K V hK hKV) ⊆ ↑V

theorem Hironaka.Manifold.isCompact_closure_shrinkBetween {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : IsCompact (closure ↑(shrinkBetween K V hK hKV))

def Hironaka.Manifold.shrinkChainAux {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K : Set M.carrier) (V : TopologicalSpace.Opens M.carrier) (hK : IsCompact K) (hKV : K ⊆ ↑V) : ℕ → { W : TopologicalSpace.Opens M.carrier // K ⊆ ↑W }

The iterated shrinks of K inside V, each carrying K ⊆ W.

Equations

• Hironaka.Manifold.shrinkChainAux K V hK hKV 0 = ⟨Hironaka.Manifold.shrinkBetween K V hK hKV, ⋯⟩
• Hironaka.Manifold.shrinkChainAux K V hK hKV j.succ = ⟨Hironaka.Manifold.shrinkBetween K (↑(Hironaka.Manifold.shrinkChainAux K V hK hKV j)) hK ⋯, ⋯⟩

noncomputable def Hironaka.Manifold.shrinkChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (K : Set M.carrier) (V : TopologicalSpace.Opens M.carrier) (hK : IsCompact K) (hKV : K ⊆ ↑V) (j : ℕ) : TopologicalSpace.Opens M.carrier

The iterated shrinks of a compact K inside an open V: shrinkChain K V hK hKV 0 ⋐ V, shrinkChain K V hK hKV (j + 1) ⋐ shrinkChain K V hK hKV j, every one relatively compact and containing K. The canonical chain of the resolution family is made of them.

Equations

• Hironaka.Manifold.shrinkChain K V hK hKV j = ↑(Hironaka.Manifold.shrinkChainAux K V hK hKV j)

theorem Hironaka.Manifold.subset_shrinkChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) (j : ℕ) : K ⊆ ↑(shrinkChain K V hK hKV j)

theorem Hironaka.Manifold.shrinkChain_zero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : shrinkChain K V hK hKV 0 = shrinkBetween K V hK hKV

theorem Hironaka.Manifold.shrinkChain_succ {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) (j : ℕ) : shrinkChain K V hK hKV (j + 1) = shrinkBetween K (shrinkChain K V hK hKV j) hK ⋯

theorem Hironaka.Manifold.closure_shrinkChain_zero_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : closure ↑(shrinkChain K V hK hKV 0) ⊆ ↑V

theorem Hironaka.Manifold.closure_shrinkChain_succ_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) (j : ℕ) : closure ↑(shrinkChain K V hK hKV (j + 1)) ⊆ ↑(shrinkChain K V hK hKV j)

theorem Hironaka.Manifold.isCompact_closure_shrinkChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) (j : ℕ) : IsCompact (closure ↑(shrinkChain K V hK hKV j))

theorem Hironaka.Manifold.shrinkChain_succ_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) (j : ℕ) : shrinkChain K V hK hKV (j + 1) ≤ shrinkChain K V hK hKV j

theorem Hironaka.Manifold.shrinkChain_antitone {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) : Antitone (shrinkChain K V hK hKV)

theorem Hironaka.Manifold.closure_shrinkChain_subset_of_lt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {K : Set M.carrier} {V : TopologicalSpace.Opens M.carrier} (hK : IsCompact K) (hKV : K ⊆ ↑V) {i j : ℕ} (h : i < j) : closure ↑(shrinkChain K V hK hKV j) ⊆ ↑(shrinkChain K V hK hKV i)

The least order bound on a compact closure, and the open where it holds

noncomputable def Hironaka.Manifold.maxOrdOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ℕ

d_U, the least bound of ord 𝓘 on the compact closure U (bddAbove_ord_on_compact): the maximal order of 𝓘 on closure U when U is nonempty, 0 when U is empty. Hironaka's d_i, the maximal integer attained by the order [Hir64, Main Theorem II(N), p. 176].

Equations

• Hironaka.Manifold.maxOrdOn T U hU = Nat.find ⋯

theorem Hironaka.Manifold.ord_le_maxOrdOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (x : M.carrier) : x ∈ closure ↑U → Manifold.IdealSheaf.ord T.I x ≤ ↑(maxOrdOn T U hU)

def Hironaka.Manifold.orderOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (D : ℕ) : TopologicalSpace.Opens M.carrier

The open {ord 𝓘 ≤ D} (upper semicontinuity of the order, isOpen_setOf_ord_le), on which the rounds from D may start.

Equations

• Hironaka.Manifold.orderOpen T D = { carrier := {x : M.carrier | Manifold.IdealSheaf.ord T.I x ≤ ↑D}, is_open' := ⋯ }

theorem Hironaka.Manifold.closure_subset_orderOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : closure ↑U ⊆ ↑(orderOpen T (maxOrdOn T U hU))

Chains of opens

theorem Hironaka.Manifold.chain_le_of_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {Ω : ℕ → TopologicalSpace.Opens X.carrier} {D : ℕ} (hΩsub : ∀ (k : ℕ), k + 1 < D → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {k j : ℕ} (hkj : k ≤ j) (hj : j < D) : Ω k ≤ Ω j

A chain with closure (Ω k) ⊆ Ω (k + 1) below D is monotone below D.

theorem Hironaka.Manifold.chain_closure_subset_of_lt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {Ω : ℕ → TopologicalSpace.Opens X.carrier} {D : ℕ} (hΩsub : ∀ (k : ℕ), k + 1 < D → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {k j : ℕ} (hkj : k < j) (hj : j < D) : closure ↑(Ω k) ⊆ ↑(Ω j)

def Hironaka.Manifold.traceOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (O V : TopologicalSpace.Opens X.carrier) : TopologicalSpace.Opens (X.restrict O).carrier

The trace of an open V of X on the open submanifold X.restrict O.

Equations

• Hironaka.Manifold.traceOn O V = { carrier := Subtype.val ⁻¹' ↑V, is_open' := ⋯ }

One round: the list, the derived triple

theorem Hironaka.Manifold.boClass_succ_of_ord_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {d : ℕ} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hord : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur.I x ≤ ↑(d + 1)) (hfin : Finite { j : cur.F.ι // cur.F.hyp j ≠ ∅ }) : Manifold.AnalyticTriple.BOClass (d + 1) cur

A triple of order ≤ d + 1 everywhere with finitely many nonempty boundary members lies in the class of BO_{n,d+1} (the hypothesis max-ord I ≤ m of [Kol07, Theorem 68]).

def Hironaka.Manifold.roundList {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {d : ℕ} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hcls : Manifold.AnalyticTriple.BOClass (d + 1) cur) (O : TopologicalSpace.Opens X.carrier) (hO : IsCompact (closure ↑O)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)

The round's list: the value of the family BO_{n,d+1} on the current triple cur at the reading open O (one round of [Hir64, Main Theorem II(N), p. 176]; [Kol07, Theorem 68]).

Equations

• Hironaka.Manifold.roundList bo cur hcls O hO = ((bo (d + 1)).functor.fam cur hcls).seqOn O hO

noncomputable def Hironaka.Manifold.derivedTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {d : ℕ} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hcls : Manifold.AnalyticTriple.BOClass (d + 1) cur) (O : TopologicalSpace.Opens X.carrier) (hO : IsCompact (closure ↑O)) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((roundList bo cur hcls O hO).stage (Fin.last (roundList bo cur hcls O hO).length))

The derived triple at the last stage of the round: the induced triple at mark d + 1 (AnalyticTriple.induced), whose ideal is Hironaka's weak transform J_{i+1} of J_i [Hir64, Main Theorem II(N), p. 176], Kollár's marked transform at the current mark (Hironaka/Resolution/Analytic/Wlo09/HironakaClauses.lean).

Equations

• Hironaka.Manifold.derivedTriple bo cur hcls O hO = (cur.pullback (X.inclusion O) ⋯).induced (d + 1) (Hironaka.Manifold.roundList bo cur hcls O hO) ⋯

theorem Hironaka.Manifold.derivedTriple_ord_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {d : ℕ} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hcls : Manifold.AnalyticTriple.BOClass (d + 1) cur) (O : TopologicalSpace.Opens X.carrier) (hO : IsCompact (closure ↑O)) (x : ((roundList bo cur hcls O hO).stage (Fin.last (roundList bo cur hcls O hO).length)).carrier) : Manifold.IdealSheaf.ord (derivedTriple bo cur hcls O hO).I x ≤ ↑d

The derived triple has order ≤ d everywhere (clause (1) of [Kol07, Theorem 68], max-ord I_r < m, the round's ord_lt): the next round applies to it on its whole manifold.

theorem Hironaka.Manifold.derivedTriple_finite {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {d : ℕ} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hcls : Manifold.AnalyticTriple.BOClass (d + 1) cur) (O : TopologicalSpace.Opens X.carrier) (hO : IsCompact (closure ↑O)) : Finite { j : (derivedTriple bo cur hcls O hO).F.ι // (derivedTriple bo cur hcls O hO).F.hyp j ≠ ∅ }

The derived triple has finitely many nonempty boundary members (finite_nonempty_totalTransformSeqFrom).

The chain lifted to a round's last stage

def Hironaka.Manifold.liftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) (V : TopologicalSpace.Opens X.carrier) : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier

The lift of an open V of X to the last stage of a list on X.restrict O: its preimage under the composite blow-down (Włodarczyk's Ũ = prin⁻¹(U), [Wlo09, Theorem 2.0.3 (1)]).

Equations

• Hironaka.Manifold.liftOpens L V = { carrier := ⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' Subtype.val ⁻¹' ↑V, is_open' := ⋯ }

theorem Hironaka.Manifold.coe_liftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) (V : TopologicalSpace.Opens X.carrier) : ↑(liftOpens L V) = ⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' Subtype.val ⁻¹' ↑V

The lift of V as a set: the preimage of V under the composite blow-down.

theorem Hironaka.Manifold.isCompact_closure_liftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) {V : TopologicalSpace.Opens X.carrier} (hV : IsCompact (closure ↑V)) (hVO : closure ↑V ⊆ ↑O) : IsCompact (closure ↑(liftOpens L V))

The lift of a relatively compact open with closure inside O is relatively compact (the composite blow-down is proper, isProperMap_stageMap).

theorem Hironaka.Manifold.closure_liftOpens_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) {V W : TopologicalSpace.Opens X.carrier} (hVW : closure ↑V ⊆ ↑W) : closure ↑(liftOpens L V) ⊆ ↑(liftOpens L W)

The lift preserves shrinking with closures.

theorem Hironaka.Manifold.range_pullbackLiftLast_subset_liftOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (V : TopologicalSpace.Opens X.carrier) (hV : Set.range ⇑ι ⊆ ↑V) (h : Set.range ⇑ι ⊆ ↑O) : Set.range ⇑(L.pullbackLiftLast (AnalyticMap.corestrict ι O h) ⋯) ⊆ ↑(liftOpens L V)

The last-stage lift of a map into V ⊆ O lands in the lift of V (range_pullbackLiftLast_subset).

def Hironaka.Manifold.liftChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (k : ℕ) : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier

The chain lifted to the last stage of L.

Equations

• Hironaka.Manifold.liftChain L Ω k = Hironaka.Manifold.liftOpens L (Ω k)

theorem Hironaka.Manifold.liftChain_isCompact {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) {Ω : ℕ → TopologicalSpace.Opens X.carrier} {d : ℕ} (hΩ : ∀ k < d + 1, IsCompact (closure ↑(Ω k))) (hΩsub : ∀ (k : ℕ), k + 1 < d + 1 → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) (hO : O = Ω d) (k : ℕ) : k < d → IsCompact (closure ↑(liftChain L Ω k))

theorem Hironaka.Manifold.liftChain_closure_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {O : TopologicalSpace.Opens X.carrier} (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) {Ω : ℕ → TopologicalSpace.Opens X.carrier} {d : ℕ} (hΩsub : ∀ (k : ℕ), k + 1 < d + 1 → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) (k : ℕ) : k + 1 < d → closure ↑(liftChain L Ω k) ⊆ ↑(liftChain L Ω (k + 1))

The rounds d ↓ along a chain, as one recursion over the current manifold

theorem Hironaka.Manifold.range_subset_chain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {Ω : ℕ → TopologicalSpace.Opens X.carrier} {d : ℕ} (hΩsub : ∀ (k : ℕ), k + 1 < d + 1 → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {ι : AnalyticMap N X} (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) : Set.range ⇑ι ⊆ ↑(Ω d)

The range of the reading map lies in every open of the chain below d + 1.

def Hironaka.Manifold.resolveFrom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (_hord : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur.I x ≤ ↑d) (_hfin : Finite { j : cur.F.ι // cur.F.hyp j ≠ ∅ }) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (_hΩ : ∀ k < d, IsCompact (closure ↑(Ω k))) (_hΩsub : ∀ (k : ℕ), k + 1 < d → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (_hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (_hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N

The rounds d, d − 1, …, 1 of the families bo on the current derived triple cur (of order ≤ d everywhere, with finitely many nonempty boundary members) along the chain Ω of relatively compact opens of the current manifold (closure (Ω k) ⊆ Ω (k + 1) below d), read on the manifold N of a local analytic isomorphism ι into Ω 0: the iteration of Hir64, Main Theorem II(N), p. 176 at decreasing maximal order, [Wlo09, Theorem 2.0.3 (1)]. Round d + 1 is the family's value at Ω d; the derived triple is the induced triple at mark d + 1 on the round's last stage; the chain and ι are lifted to that stage; the value is the round's list pulled back along ι followed by the rounds from d, pulled back along the last-stage lift of ι; the second factor lives on the first factor's last stage by construction.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Manifold.resolveFrom bo 0 x_1 x_8 x_2 x_3 x_9 x_10 x_5 x_6 x_7 = AnalyticManifold.BlowUpSequence.nil x_4

Admissible chains and the value along one; the canonical chain; the value on an open

structure Hironaka.Manifold.ResolveChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) : Type u

An admissible shrinking chain for (T, U): D rounds, opens W 0 ⊆ ⋯ ⊆ W D with compact closures, closure (W k) ⊆ W (k + 1), U ≤ W 0, and ord 𝓘 ≤ D on the outermost open (so the triple restricted to it lies in the class of BO_{n,D} when D ≥ 1). Włodarczyk's open neighbourhood U ⊃ Z of [Wlo09, Theorem 2.0.3 (1)], read D times.

• D : ℕ

  The number of rounds.

• W : ℕ → TopologicalSpace.Opens M.carrier

  The opens, W 0 the innermost, W D the outermost.

• isCompact_closure (k : ℕ) : k ≤ self.D → IsCompact (closure ↑(self.W k))

  Compact closures.

• closure_subset (k : ℕ) : k < self.D → closure ↑(self.W k) ⊆ ↑(self.W (k + 1))

  Shrinking with closures.

• le_zero : U ≤ self.W 0

  U lies in the innermost open.

• ord_le (x : M.carrier) : x ∈ self.W self.D → Manifold.IdealSheaf.ord T.I x ≤ ↑self.D

  The order bound on the outermost open.

theorem Hironaka.Manifold.ResolveChain.le_of_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) {k j : ℕ} (hkj : k ≤ j) (hj : j ≤ c.D) : c.W k ≤ c.W j

theorem Hironaka.Manifold.ResolveChain.le_outer {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) (k : ℕ) (hk : k ≤ c.D) : c.W k ≤ c.W c.D

theorem Hironaka.Manifold.ResolveChain.closure_subset_of_lt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) {k j : ℕ} (hkj : k < j) (hj : j ≤ c.D) : closure ↑(c.W k) ⊆ ↑(c.W j)

noncomputable def Hironaka.Manifold.ResolveChain.outerTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict (c.W c.D))

The triple restricted to the outermost open.

Equations

• c.outerTriple = T.pullback (M.inclusion (c.W c.D)) ⋯

theorem Hironaka.Manifold.ResolveChain.outerTriple_ord_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) (x : (M.restrict (c.W c.D)).carrier) : Manifold.IdealSheaf.ord c.outerTriple.I x ≤ ↑c.D

The order bound restricts to the outermost open.

theorem Hironaka.Manifold.ResolveChain.outerTriple_finite {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) : Finite { j : c.outerTriple.F.ι // c.outerTriple.F.hyp j ≠ ∅ }

Finitely many boundary members meet the relatively compact outermost open (boClass_pullback_inclusion).

def Hironaka.Manifold.ResolveChain.trace {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) (k : ℕ) : TopologicalSpace.Opens (M.restrict (c.W c.D)).carrier

The chain as opens of the outermost open.

Equations

• c.trace k = Hironaka.Manifold.traceOn (c.W c.D) (c.W k)

theorem Hironaka.Manifold.ResolveChain.isCompact_closure_trace {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) (k : ℕ) (hk : k < c.D) : IsCompact (closure ↑(c.trace k))

theorem Hironaka.Manifold.ResolveChain.closure_trace_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) (k : ℕ) (hk : k + 1 < c.D) : closure ↑(c.trace k) ⊆ ↑(c.trace (k + 1))

theorem Hironaka.Manifold.ResolveChain.le_outerOpen {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) : U ≤ c.W c.D

theorem Hironaka.Manifold.ResolveChain.range_restrictLE_subset_trace {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {U : TopologicalSpace.Opens M.carrier} (c : ResolveChain T U) : Set.range ⇑(M.restrictLE ⋯) ⊆ ↑(c.trace 0)

noncomputable def Hironaka.Manifold.resolveSeqOnAlong {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bo : (d : ℕ) → BOanFam 𝕜 n d) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (c : ResolveChain T U) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U)

The value along an admissible chain: the rounds c.D, …, 1 on the triple restricted to the outermost open, along the chain, read on U, the empty blow-ups erased ([Wlo09, Theorem 2.0.3 (1)]; the empty blow-up convention [Kol07, 32]). Canonicity (Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean) shows that it does not depend on the chain.

Equations

• Hironaka.Manifold.resolveSeqOnAlong bo T U c = (Hironaka.Manifold.resolveFrom bo c.D c.outerTriple ⋯ ⋯ c.trace ⋯ ⋯ (M.restrictLE ⋯) ⋯ ⋯).eraseEmpty

theorem Hironaka.Manifold.noEmptyCenters_resolveSeqOnAlong {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bo : (d : ℕ) → BOanFam 𝕜 n d) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (c : ResolveChain T U) : (resolveSeqOnAlong bo T U c).NoEmptyCenters

noncomputable def Hironaka.Manifold.canonicalResolveChain {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ResolveChain T U

The canonical chain: d_U + 1 iterated shrinks of closure U inside {ord 𝓘 ≤ d_U}, the k-th open being the (d_U − k)-th shrink, so the innermost is the last shrink and the outermost the first.

Equations

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

noncomputable def Hironaka.Manifold.resolveSeqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bo : (d : ℕ) → BOanFam 𝕜 n d) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U)

The value of the resolution family on the relatively compact open U: the rounds d_U, …, 1 along the canonical chain, read on U, the empty blow-ups erased (Hir64, Main Theorem II(N), p. 176; [Wlo09, Theorem 2.0.3 (1)]). Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean proves its compatibility under restriction and bundles it into resolveFam.

Equations

• Hironaka.Manifold.resolveSeqOn bo T U hU = Hironaka.Manifold.resolveSeqOnAlong bo T U (Hironaka.Manifold.canonicalResolveChain T U hU)

theorem Hironaka.Manifold.noEmptyCenters_resolveSeqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bo : (d : ℕ) → BOanFam 𝕜 n d) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (resolveSeqOn bo T U hU).NoEmptyCenters

The value has no empty blow-ups (the empty blow-up convention [Kol07, 32]).