The multiple locus of a family of hypersurfaces

HypersurfaceFamily.singularLocus F, the set of points lying on two distinct components of the family — the analytic counterpart of the multiple locus of a divisor family in the Hironaka library (here a Set; closedness, for locally finite families, is left to the uses). For an snc family it is exactly the locus where the support |F| is not a smooth hypersurface. Kollár's principalization is an isomorphism "over X ∖ cosupp I" [Kol07, Theorem 35 (3)]; when the boundary components are first made disjoint by the preliminary blow-ups of [Kol07, 72], whose centres — the k-fold meet loci of the components — lie in Sing F, the isomorphism holds over the complement of cosupp 𝓘 ∪ Sing F.

def Manifold.HypersurfaceFamily.singularLocus {M : Type u} (F : HypersurfaceFamily M) : Set M

The multiple locus Sing F of a family of hypersurfaces: the points lying on two distinct components. For an snc family it is the locus where the support is not a smooth hypersurface; the preliminary blow-ups that make the components of the boundary disjoint [Kol07, 72] have their centres inside it.

Equations

• F.singularLocus = {x : M | ∃ (i : F.ι) (j : F.ι), i ≠ j ∧ x ∈ F.hyp i ∧ x ∈ F.hyp j}

theorem Manifold.HypersurfaceFamily.mem_singularLocus {M : Type u} {F : HypersurfaceFamily M} {x : M} : x ∈ F.singularLocus ↔ ∃ (i : F.ι) (j : F.ι), i ≠ j ∧ x ∈ F.hyp i ∧ x ∈ F.hyp j

theorem Manifold.HypersurfaceFamily.singularLocus_subset_support {M : Type u} (F : HypersurfaceFamily M) : F.singularLocus ⊆ F.support

The multiple locus lies in the support.

theorem Manifold.HypersurfaceFamily.singularLocus_empty {M : Type u} : (empty M).singularLocus = ∅

The empty family has empty multiple locus.