The data consumed by Step 2.2 of the proof of Theorem 103

Step 2.2 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.2]) applies, at the last stage of the sequence of Step 2.1, Lemma 102 to the triple (X_r, I_r, H_r + E_r) at the member H_r, the transform of the hypersurface of maximal contact. Kollár declares H the first member of H + E; the library appends it as the greatest member of the boundary, and the class stepHClass (Step22Defs.lean) is that of triples with a greatest member. What the machinery of Step 2.2 in the compatible-family form (Step22Fam.lean to LocalFunctorFam.lean) uses of the family applied at that member is four of the clauses of BDanFamData (FamilyData.lean): the value, the order clause in the form "of order ≥ s" ([Kol07, Definition 66 (1′)–(4′)]; it enters the uniqueness of the hypersurface of maximal contact, [Kol07, Theorem 97]), the commutation with local analytic isomorphisms and the indifference to empty boundary members. Neither the exactness of the order nor Lemma 102 (1) is used there. This matters because the modified algorithm of Włodarczyk (the proof of [Wlo09, Theorem 7.4.1]: the components on which the ideal has become the ideal of a smooth hypersurface are left alone) supplies data for the same step which satisfy the four clauses but not the other two.

• HFamData ψ₀ s — the four clauses; BDanFamData.toHFamData (Lemma 102's family is an instance).
• HFData ψ₀ s — the data of Step 2 at the mark s: Step 2.1's data bd₁ : BDanFamData ψ₀ s and the data hf : HFamData ψ₀ (tuningParam s) for the hypersurface step at the re-tuned mark (Step 2.2 begins by replacing I by W(I) once more); HFData.ofBDanFamData takes both from Lemma 102's data at every mark, as Kollár does, with the unfolding lemmas ofBDanFamData_bd₁, ofBDanFamData_hf.
• HFamData.hstepFunctor — the family at the greatest member, as a family functor on the class stepHClass s; its commutation with local analytic isomorphisms is HFamData.hstepFunctor_commutesWithLocalIsos (Step22FamFunctoriality.lean).

The assembly of Step 2 over HFData is in Step22Fam.lean and its successors; the data of Włodarczyk's modified step at the mark 1 are BMOmod.hFamDataMod (Modified/StepBData.lean).

structure Hironaka.Manifold.HFamData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (s : ℕ) : Type (max (u + 1) u_1)

The data consumed by Step 2.2 of the proof of [Kol07, Theorem 103] at the mark s: a compatible family on every triple of the class of BO_{n,s} and every member of its boundary, which on every relatively compact open is a smooth blow-up sequence of order ≥ s for the restricted triple ([Kol07, Definition 66 (1′)–(4′)]), commutes with local analytic isomorphisms (both bullets of [Kol07, 34.1] in one clause per open) and is indifferent to empty boundary members. These are the clauses of BDanFamData without the exactness of the order and without Lemma 102 (1).

• fam {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) : Manifold.AnalyticTriple.BOClass s T → T.F.ι → CompatibleFamily T

  The value at the member j as a compatible family.

• isOfOrderGe {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((self.fam T hT j).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf

  [Kol07, Definition 66 (1′)–(4′)] per open: the value on U is of order ≥ s for the restricted triple (U, 𝓘|_U, E|_U).

• commutesWithLocalIsos {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT : Manifold.AnalyticTriple.BOClass s T) (hT' : Manifold.AnalyticTriple.BOClass s (T.pullback g hg)) (j : T.F.ι) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : (self.fam (T.pullback g hg) hT' j).seqOn U' hU' = (((self.fam T hT j).seqOn (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

  Both bullets of [Kol07, 34.1] in one clause per open, the member index kept: along a local analytic isomorphism g, the value of the pulled-back triple on a relatively compact open is the pull-back of the value on the image open, with empty blow-ups deleted.

• indifferentToEmptyMembers {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) : (∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) → (∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) → ∀ (hT : Manifold.AnalyticTriple.BOClass s T) (hT' : Manifold.AnalyticTriple.BOClass s { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) (i : F'.ι) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), (self.fam T hT (e i)).seqOn U hU = (self.fam { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hT' i).seqOn U hU

  Indifference to empty boundary members, per open: deleting empty members along an order embedding of the index types does not change the value at a kept member.

def Hironaka.Manifold.BDanFamData.toHFamData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) : HFamData ψ₀ s

Lemma 102's family data satisfy the four clauses of HFamData (its exact order gives the order clause).

Equations

• bd.toHFamData = { fam := fun {M : AnalyticManifold 𝕜 E} => bd.fam, isOfOrderGe := ⋯, commutesWithLocalIsos := ⋯, indifferentToEmptyMembers := ⋯ }

structure Hironaka.Manifold.HFData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (s : ℕ) : Type (max (u + 1) u_1)

The data of Step 2 of the proof of [Kol07, Theorem 103] in the compatible-family form, at the mark s: the data of Step 2.1 (Lemma 102's family at the mark s, Kol07, Theorem 103, Step 2.1) and the data for the hypersurface step of Step 2.2 at the re-tuned mark tuningParam s ([Kol07, 104, Step 2.2]: "we can again replace I by W(I)"). Kollár takes both from Lemma 102's data at every mark (HFData.ofBDanFamData); Włodarczyk's modified algorithm (the proof of [Wlo09, Theorem 7.4.1]) takes the second from the modified marked resolution (BMOmod.hFamDataMod).

• bd₁ : BDanFamData ψ₀ s

  The data of Step 2.1 at the mark s.

• hf : HFamData ψ₀ (IsLocalRing.tuningParam s)

  The data for the hypersurface step at the re-tuned mark tuningParam s.

def Hironaka.Manifold.HFData.ofBDanFamData {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (s : ℕ) : HFData ψ₀ s

The data of Step 2 as Kollár takes them: Lemma 102's family data at the mark s and at the re-tuned mark.

Equations

• Hironaka.Manifold.HFData.ofBDanFamData bd s = { bd₁ := bd s, hf := (bd (IsLocalRing.tuningParam s)).toHFamData }

@[simp]

theorem Hironaka.Manifold.HFData.ofBDanFamData_bd₁ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (s : ℕ) : (ofBDanFamData bd s).bd₁ = bd s

@[simp]

theorem Hironaka.Manifold.HFData.ofBDanFamData_hf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (bd : (s : ℕ) → BDanFamData ψ₀ s) (s : ℕ) : (ofBDanFamData bd s).hf = (bd (IsLocalRing.tuningParam s)).toHFamData

theorem Hironaka.Manifold.HFamData.fam_congr_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) {M : AnalyticManifold 𝕜 E} {T₁ T₂ : Manifold.AnalyticTriple ψ₀ M} (e : T₁ = T₂) (h₁ : Manifold.AnalyticTriple.BOClass s T₁) (h₂ : Manifold.AnalyticTriple.BOClass s T₂) (j₁ : T₁.F.ι) (j₂ : T₂.F.ι) (hj : j₁ ≍ j₂) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (hf.fam T₁ h₁ j₁).seqOn U hU = (hf.fam T₂ h₂ j₂).seqOn U hU

The value of the family depends only on the triple and the member: transport along an equality of triples and a matching equality of members.

noncomputable def Hironaka.Manifold.HFamData.hstepFunctor {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => BO.stepHClass s

The family applied at the greatest member of the boundary, as a family functor on the class stepHClass s of triples of BOClass s with a greatest member; stepHFamFunctor (Step22Fam.lean) is this functor at Lemma 102's data.

Equations

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

theorem Hironaka.Manifold.HFamData.hstepFunctor_fam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : BO.stepHClass s T) : hf.hstepFunctor.fam T hT = hf.fam T ⋯ (BO.greatestIdx hT)