Finiteness over relatively compact open subsets

On a non-compact manifold the finite index sets and the maximal order of Kollár's triples are not available globally. They are restored over an open subset U with compact closure, the setting of Bierstone–Milman's "relatively quasi-compact open subset" ([BM97, Theorem 1.6] and the remark following it) and of Kollár's "small neighborhoods of compact sets" ([Kol07, 44]): only finitely many members of a locally finite family meet the compact closure, and the order of an ideal sheaf that is nonzero at every point is bounded on a compact set, being finite at each point and upper semicontinuous ({ord ≤ k} is open because {ord ≥ k + 1} is the cosupport of the derivative ideal sheaf D^k 𝓘 (cosupport_iteratedDeriv), which is closed).

• AnalyticTriple.boClass_iff — the class BOClass m unfolded;
• HypersurfaceFamily.IsSnc.finite_meeting_compact — only finitely many members of a family with simple normal crossings meet a compact set;
• IdealSheaf.bddAbove_ord_on_compact — the order of an ideal sheaf nonzero everywhere is bounded on a compact set;
• boClass_pullback_inclusion, exists_boClass_pullback_inclusion — the restriction of a triple to an open subset with compact closure lies in BOClass m for m a bound of the order on U, and for some m.

This is what makes the compatible-family form of the order-reduction functors meaningful: the value on each relatively compact open is that of a functor on BOClass m for a suitable m (Functor/Family.lean, BOanFamOfInput.lean).

theorem Manifold.AnalyticTriple.boClass_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (m : ℕ) (T : AnalyticTriple ψ₀ M) : BOClass m T ↔ 1 ≤ m ∧ (∀ (x : ↑↧M.carrier), IdealSheaf.ord T.I x ≤ ↑m) ∧ Finite { j : T.F.ι // T.F.hyp j ≠ ∅ }

The class of BO_{n,m} unfolded ([Kol07, Theorem 103]: "dim X = n, max-ord I ≤ m"): a triple is in BOClass m iff 1 ≤ m, ord 𝓘 ≤ m at every point and only finitely many members of E are nonempty.

theorem Manifold.HypersurfaceFamily.IsSnc.finite_meeting_compact {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} (hF : IsSnc ψ₀ F) {K : Set M.carrier} (hK : IsCompact K) : {j : F.ι | (F.hyp j ∩ K).Nonempty}.Finite

Only finitely many members of a family of hypersurfaces with simple normal crossings meet a compact set: the family is locally finite.

theorem Manifold.IdealSheaf.bddAbove_ord_on_compact {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} (hI : IsNonzeroEverywhere I) {K : Set M.carrier} (hK : IsCompact K) : ∃ (m : ℕ), ∀ x ∈ K, ord I x ≤ ↑m

The order of an ideal sheaf that is nonzero at every point is bounded on a compact set: it is finite at every point and upper semicontinuous (isOpen_setOf_ord_le), so finitely many of the open sets {ord ≤ ord x} cover the compact set. Not in the sources as such; the analytic substitute for Kollár's max-ord I.

theorem Hironaka.Manifold.boClass_pullback_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {m : ℕ} (hm : 1 ≤ m) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hord : ∀ x ∈ ↑U, Manifold.IdealSheaf.ord T.I x ≤ ↑m) : Manifold.AnalyticTriple.BOClass m (T.pullback (M.inclusion U) ⋯)

The restriction of a triple to an open subset U with compact closure, on which the order of 𝓘 is at most m ≥ 1, lies in the class BOClass m (the setting of the remark after [BM97, Theorem 1.6]): the pull-back along the inclusion has the order of 𝓘 at the image, and a member of the pulled-back family is nonempty only if the member meets U ⊆ closure U, which finitely many do.

theorem Hironaka.Manifold.exists_boClass_pullback_inclusion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ∃ (m : ℕ), Manifold.AnalyticTriple.BOClass m (T.pullback (M.inclusion U) ⋯)

The restriction of a triple to an open subset with compact closure lies in the class BOClass m for some m ([BM97, Theorem 1.6] and the remark after it; [Kol07, 44]): the order of 𝓘 is bounded on the compact closure.