Order reduction on manifolds: Step 2.2 of the proof of Theorem 103

Step 2.2 of the proof of [Kol07, Theorem 103]: once H + E has simple normal crossings, "we restrict everything to the birational transform of H" and obtain order reduction from Lemma 102 by the induction on the dimension. Two remarks of Kollár govern the construction: under a smooth blow-up of order m the birational transform of a smooth hypersurface of maximal contact is again one (Step 2 of the proof), and one should not pick new hypersurfaces of maximal contact after a blow-up but stick with the birational transforms of the old ones (the Warning of [Kol07, 104]). This module provides the vocabulary of the construction, which is made in the compatible-family form in Step22Fam.lean.

• HypersurfaceFamily.finite_nonempty_append, HypersurfaceFamily.appendIdx, HypersurfaceFamily.isSnc_append_of_hasSncWithProper — appending a hypersurface having proper simple normal crossings with a family keeps the family with simple normal crossings (at a point of H the proper chart is a chart of the appended family, its indices those of the members of F through the point and the coordinate of H; away from H the family's own chart serves) and keeps the nonempty members finite. Not in the sources.
• BO.stepHClass, BO.greatestIdx — the class of triples of BOClass s whose boundary has a greatest member, and that member, at which Lemma 102 is applied (the greatest member of F + H is H); stepHClass_tuned — the class is kept by Kollár's re-tuning "we can again replace I by W(I)" ([Kol07, 104, Step 2.2]; Kollár re-tunes at s!; the library's mark is tuningParam s, as in Tuned.lean). Kollár declares H the first member of H + E (index 0); the library appends it as the greatest member, a convention that only fixes the index at which Lemma 102 is applied.

The clauses of Theorem 103 for Step 2 in the compatible-family form are proved in Step22Fam*.lean, Step2Assembly*.lean and FamilyIndependence.lean; Step 3 of the proof assembles the local functors in GlobalizeFam.lean.

Appending a hypersurface with proper simple normal crossings

theorem Manifold.HypersurfaceFamily.finite_nonempty_append {M : Type u} (F : HypersurfaceFamily M) (H : Set M) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) : Finite { k : (F.append H).ι // (F.append H).hyp k ≠ ∅ }

Appending one hypersurface keeps the nonempty members of a family finite.

def Manifold.HypersurfaceFamily.appendIdx {n : ℕ} {M : Type u} (F : HypersurfaceFamily M) (H : Set M) (a : M) (cF : { j : F.ι // a ∈ F.hyp j } → Fin n) (cH : Fin n) (k : { k : (F.append H).ι // a ∈ (F.append H).hyp k }) : Fin n

Chart indices for F + H at a point a: the index cF j for a member E^j of F through a, and the index cH for H.

Equations

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

theorem Manifold.HypersurfaceFamily.isSnc_append_of_hasSncWithProper {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : Type u} {ψ : E ≃L[𝕜] Fin n → 𝕜} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {H : Set M} (hF : IsSnc ψ F) (hH : IsClosedSubmanifold ψ H 1) (hFH : HasSncWithProper ψ F H 1) : IsSnc ψ (F.append H)

Appending a hypersurface H having proper simple normal crossings with F keeps the family with simple normal crossings ([Kol07, Definition 24]; this is Kollár's observation in Step 2.1 of the proof of [Kol07, Theorem 103] that the new exceptional divisors have simple normal crossings with the transforms of H, so that H_r + E_r has simple normal crossings): at a point of H the proper chart (adapted to H, a chart of F whose indices avoid the coordinate of H) is a chart of F + H; away from H the chart of F serves.

Appending a member away from a hypersurface

theorem Manifold.HypersurfaceFamily.hasSncWithProper_append_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} {S Z : Set M.carrier} (hFS : HasSncWithProper ψ F S 1) (hZ : ∀ a ∈ S, a ∉ Z) : HasSncWithProper ψ (F.append Z) S 1

Appending a member missing the hypersurface S keeps proper simple normal crossings with S: the proper chart of F at a point of S serves, the appended member passing through no point of S.

theorem Hironaka.Manifold.le_toLex_inr {ι : Type u} [LinearOrder ι] (k : ι ⊕ₗ PUnit.{u + 1}) : k ≤ toLex (Sum.inr PUnit.unit)

The appended member is the greatest index of F + H (the lexicographic sum puts the right summand last).

theorem Hironaka.Manifold.finite_nonempty_totalTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin (S.length + 1)) : Finite { k : (S.totalTransformSeq i).ι // (S.totalTransformSeq i).hyp k ≠ ∅ }

The family of exceptional divisors (from the empty start) has finitely many nonempty members at every stage.

The greatest member of the boundary

def Hironaka.Manifold.BO.stepHClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (s : ℕ) {M : AnalyticManifold 𝕜 E} : Manifold.AnalyticTriple ψ₀ M → Prop

The class of triples of BOClass s whose boundary has a greatest member: the triples (X, I, H + E) to which Kollár applies BD_{n,m,0} in Step 2.2 of the proof of [Kol07, Theorem 103], the appended H being the greatest member.

Equations

• Hironaka.Manifold.BO.stepHClass s T = (Manifold.AnalyticTriple.BOClass s T ∧ ∃ (j : T.F.ι), ∀ (k : T.F.ι), k ≤ j)

noncomputable def Hironaka.Manifold.BO.greatestIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} {T : Manifold.AnalyticTriple ψ₀ M} (hT : stepHClass s T) : T.F.ι

The greatest member of the boundary of a triple of the class.

Equations

• Hironaka.Manifold.BO.greatestIdx hT = Classical.choose ⋯

theorem Hironaka.Manifold.BO.le_greatestIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} {T : Manifold.AnalyticTriple ψ₀ M} (hT : stepHClass s T) (k : T.F.ι) : k ≤ greatestIdx hT

theorem Hironaka.Manifold.BO.greatestIdx_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} {T : Manifold.AnalyticTriple ψ₀ M} (hT : stepHClass s T) {j : T.F.ι} (hj : ∀ (k : T.F.ι), k ≤ j) : greatestIdx hT = j

The greatest member is unique.

Step 2.2

theorem Hironaka.Manifold.BO.stepHClass_tuned {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} [FiniteDimensional 𝕜 E] {T : Manifold.AnalyticTriple ψ₀ M} (hT : stepHClass s T) : stepHClass (IsLocalRing.tuningParam s) (T.tuned s ⋯)

A triple of the class tunes into the class at the mark tuningParam s: the boundary and its index set are kept by the tuning.