Order reduction on manifolds: the members processed by Step 2.1 of the proof of Theorem 103

Step 2.1 of the proof of [Kol07, Theorem 103] clears the boundary from the cosupport: for E = ∑_{i=1}^s E^i, "we apply (102) to each E^i", obtaining at the end a blow-up sequence Π : X_r → X with cosupp(I_r, m) disjoint from Π^{-1}_* E, the members being taken in the order of the index set of E. On analytic manifolds the boundary of a triple has a linearly ordered index set and, on the class BOClass m, only finitely many nonempty members; the nonempty members are processed in the order of the index set and the empty ones are skipped.

• HypersurfaceFamily.nonemptyFinset, HypersurfaceFamily.nonemptyList — the nonempty members of a family with finitely many of them, as a finite set and as the list sorted by the order of the index set.

Step 2.1 itself is constructed in the compatible-family form, over data bd : BDanFamData ψ₀ s for the functor BD_{n,s,j} of [Kol07, Lemma 102], in Step21Fam.lean; Step 2.2 follows in Step22Fam.lean.

noncomputable def Manifold.HypersurfaceFamily.nonemptyFinset {M : Type u} (F : HypersurfaceFamily M) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) : Finset F.ι

The finite set of nonempty members of a family with finitely many of them.

Equations

• F.nonemptyFinset hF = ⋯.toFinset

theorem Manifold.HypersurfaceFamily.mem_nonemptyFinset {M : Type u} (F : HypersurfaceFamily M) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) (j : F.ι) : j ∈ F.nonemptyFinset hF ↔ F.hyp j ≠ ∅

noncomputable def Manifold.HypersurfaceFamily.nonemptyList {M : Type u} (F : HypersurfaceFamily M) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) : List F.ι

The nonempty members of a family with finitely many of them, listed in the order of the index set (Kollár uses the ordering of the index set of E in Step 2.1 of the proof of [Kol07, Theorem 103]).

Equations

• F.nonemptyList hF = (F.nonemptyFinset hF).sort fun (x1 x2 : F.ι) => x1 ≤ x2

theorem Manifold.HypersurfaceFamily.mem_nonemptyList {M : Type u} (F : HypersurfaceFamily M) (hF : Finite { j : F.ι // F.hyp j ≠ ∅ }) (j : F.ι) : j ∈ F.nonemptyList hF ↔ F.hyp j ≠ ∅