The m-fold meet locus as a closed submanifold

Kollár's disjoining blows up "the subset where m of the E_i intersect" at a stage where no point lies on m + 1 of them, and this subset is smooth since the E_i "do not have any (m+1)-fold intersections" [Kol07, 72]. Under that hypothesis the m-fold meet locus is a closed submanifold of codimension m with which the family has simple normal crossings: at a point a of the locus exactly m members pass, and the snc chart of the family at a, shrunk to a neighbourhood where every member through a nearby point already passes through a (local finiteness), exhibits the locus as the coordinate subspace of the m coordinates of those members. This module proves that chart statement (IsSnc.exists_adaptedChart_meetLocus) and its two consequences (IsSnc.isClosedSubmanifold_meetLocus, IsSnc.hasSncWith_meetLocus) — the centre of each disjoining blow-up is a closed submanifold having simple normal crossings with the boundary, as the order-reduction algorithm requires of its centres [Kol07, Definition 66 (3)].

theorem Manifold.HypersurfaceFamily.IsSnc.exists_nhds_forall_mem_imp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (a : M) : ∃ (V : Set M), IsOpen V ∧ a ∈ V ∧ ∀ x ∈ V, ∀ (j : F.ι), x ∈ F.hyp j → a ∈ F.hyp j

Near a point a, every member through a nearby point passes through a: local finiteness of the family (the members missing a that meet a neighbourhood are finitely many, and their complements cut the neighbourhood down). The strengthening of IsSnc.exists_nhds_support_eq the meet loci need.

theorem Manifold.HypersurfaceFamily.IsSnc.isClosed_meetLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (m : ℕ) : IsClosed (F.meetLocus m)

The m-fold meet locus of an snc family is closed: near a point off it, a point on m members would put the point itself on those m members.

theorem Manifold.HypersurfaceFamily.mem_of_mem_hyp_of_meetLocus_succ_eq_empty {M : Type u} {F : HypersurfaceFamily M} {m : ℕ} (hm : F.meetLocus (m + 1) = ∅) {a : M} {s : Finset F.ι} (hs : s.card = m) (has : ∀ j ∈ s, a ∈ F.hyp j) {j : F.ι} (haj : a ∈ F.hyp j) : j ∈ s

Where no point lies on m + 1 members, the members through a point of the m-fold locus are exactly the m witnesses: any further member through the point would make m + 1.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.restrOpen_of_isOpen {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) {s : Set M} (hs : IsOpen s) (has : a ∈ s) : IsSncChartAt ψ F (φ.restrOpen s hs) a c

The restriction of an snc chart at a to an open set containing a is an snc chart at a, for any charted space (IsSncChartAt.restrOpen is stated for a bundled analytic manifold; the proof is the same — the maximal atlas is closed under restriction to opens).

theorem Manifold.HypersurfaceFamily.IsSnc.exists_adaptedChart_meetLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {m : ℕ} (hm : F.meetLocus (m + 1) = ∅) {a : M} (ha : a ∈ F.meetLocus m) : ∃ (φ : OpenPartialHomeomorph M E) (σ : Fin m ↪ Fin n) (cidx : { j : F.ι // a ∈ F.hyp j } → Fin n), IsAdaptedChart ψ (F.meetLocus m) φ σ ∧ IsSncChartAt ψ F φ a cidx ∧ Set.range ⇑σ = Set.range cidx

Kollár's "Z_t is the subset where k − t of the E_i intersect", a smooth subvariety [Kol07, 72]: where no point lies on m + 1 members, at every point a of the m-fold meet locus there is a chart, an snc chart of the family at a, adapted to the locus with the m coordinates of the members through a as its block — the locus is, near a, the intersection of the m coordinate hyperplanes. The block's index set is exactly the set of coordinate indices of the members through a.

theorem Manifold.HypersurfaceFamily.IsSnc.isClosedSubmanifold_meetLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {m : ℕ} (hm : F.meetLocus (m + 1) = ∅) : IsClosedSubmanifold ψ (F.meetLocus m) m

Where no point lies on m + 1 members, the m-fold meet locus is a closed submanifold of codimension m (possibly empty) [Kol07, 72].

theorem Manifold.HypersurfaceFamily.IsSnc.hasSncWith_meetLocus {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {m : ℕ} (hm : F.meetLocus (m + 1) = ∅) : HasSncWith ψ F (F.meetLocus m) m

Where no point lies on m + 1 members, the family has simple normal crossings with its m-fold meet locus — the condition on the centre of each disjoining blow-up ([Kol07, 72]; the hypothesis on the centres in [Kol07, Definition 66 (3)]).