The m-fold meet loci of a family of hypersurfaces

Kollár's preliminary blow-ups make the components E_1, …, E_k of the boundary disjoint by blowing up, in turn, "the subset where m of the E_i intersect" for m = k, k − 1, …, 2 [Kol07, 72]. This module defines that subset for a family of hypersurfaces — HypersurfaceFamily.meetLocus F m, the points lying on at least m distinct members — and proves its elementary properties: the cases m = 0, 1, 2 (everything, the support, the multiple locus sing of Hironaka/Manifold/Snc/Sing.lean), monotonicity in m, and emptiness beyond the number of nonempty members. That the m-fold locus is a closed submanifold of codimension m with which the family has simple normal crossings, where no point lies on m + 1 members, is proved in MeetLocusChart.lean of this directory; the disjoining sequence itself is assembled in Disjoin.lean.

def Manifold.HypersurfaceFamily.meetLocus {M : Type u} (F : HypersurfaceFamily M) (m : ℕ) : Set M

Kollár's "the subset where m of the E_i intersect" [Kol07, 72]: the set of points lying on at least m distinct members of the family — witnessed by a finite set of m indices all of whose members pass through the point. For m = 2 it is the multiple locus sing; for m = 0 it is everything; beyond the number of nonempty members it is empty.

Equations

• F.meetLocus m = {x : M | ∃ (s : Finset F.ι), s.card = m ∧ ∀ j ∈ s, x ∈ F.hyp j}

theorem Manifold.HypersurfaceFamily.mem_meetLocus {M : Type u} {F : HypersurfaceFamily M} {m : ℕ} {x : M} : x ∈ F.meetLocus m ↔ ∃ (s : Finset F.ι), s.card = m ∧ ∀ j ∈ s, x ∈ F.hyp j

theorem Manifold.HypersurfaceFamily.hyp_ne_empty_of_mem {M : Type u} {F : HypersurfaceFamily M} {j : F.ι} {x : M} (hx : x ∈ F.hyp j) : F.hyp j ≠ ∅

A member through a point is nonempty.

theorem Manifold.HypersurfaceFamily.meetLocus_zero {M : Type u} (F : HypersurfaceFamily M) : F.meetLocus 0 = Set.univ

Every point lies on at least zero members.

theorem Manifold.HypersurfaceFamily.meetLocus_one {M : Type u} (F : HypersurfaceFamily M) : F.meetLocus 1 = F.support

The 1-fold locus is the support of the family.

theorem Manifold.HypersurfaceFamily.meetLocus_two {M : Type u} (F : HypersurfaceFamily M) : F.meetLocus 2 = F.singularLocus

The 2-fold locus is the multiple locus sing (Hironaka/Manifold/Snc/Sing.lean).

theorem Manifold.HypersurfaceFamily.meetLocus_antitone {M : Type u} (F : HypersurfaceFamily M) : Antitone F.meetLocus

Lying on m' members implies lying on m of them for m ≤ m'.

theorem Manifold.HypersurfaceFamily.meetLocus_subset_singularLocus {M : Type u} (F : HypersurfaceFamily M) {m : ℕ} (hm : 2 ≤ m) : F.meetLocus m ⊆ F.singularLocus

For m ≥ 2 the m-fold locus lies in the multiple locus.

theorem Manifold.HypersurfaceFamily.meetLocus_eq_empty_of_forall_card_lt {M : Type u} (F : HypersurfaceFamily M) {m : ℕ} (h : ∀ (x : M) (s : Finset F.ι), (∀ j ∈ s, x ∈ F.hyp j) → s.card < m) : F.meetLocus m = ∅

If no m distinct members pass through any point, the m-fold locus is empty.

theorem Manifold.HypersurfaceFamily.meetLocus_eq_empty_of_finite_nonempty {M : Type u} (F : HypersurfaceFamily M) [Finite { j : F.ι // F.hyp j ≠ ∅ }] : F.meetLocus (Nat.card { j : F.ι // F.hyp j ≠ ∅ } + 1) = ∅

With finitely many nonempty members, no point lies on more members than there are nonempty ones: the (k + 1)-fold locus is empty for k the number of nonempty members (Kollár's E_1, …, E_k, the finitely many irreducible components of E [Kol07, 72]; on an analytic manifold the boundary has finitely many members over a relatively compact open).