The meet locus of a subfamily as a centre

At the t-th disjoining step of [Kol07, 72] the current divisor is the total transform (the strict transforms of the components of E together with the exceptional divisors introduced so far), while the centre is the meet locus of the strict transforms alone; the centre must have simple normal crossings with the whole current divisor [Kol07, Definition 66 (3)]. This module is the subfamily form of MeetLocusChart.lean: for an snc family G and a predicate p on its members, where no point lies on m + 1 of the p-members, at every point of the m-fold meet locus of the p-members there is a chart adapted to that locus which is an snc chart of the whole family G — so the locus is a closed submanifold of codimension m and G has snc with it (IsSnc.hasSncWith_meetLocus_subfamily). With p := fun _ => True this is the statement of MeetLocusChart.lean. Also: the subfamily of an snc family is snc (IsSnc.subfamily). Used for the centres of the disjoining blow-ups (DisjoinBoundary.lean) and of the monomial step of the order reduction.

theorem Manifold.HypersurfaceFamily.IsSnc.subfamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {G : HypersurfaceFamily M} (hG : IsSnc ψ G) (p : G.ι → Prop) : IsSnc ψ (G.subfamily p)

The subfamily of an snc family is snc.

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

The subfamily form of IsSnc.exists_adaptedChart_meetLocus [Kol07, 72]: where no point lies on m + 1 of the p-members, at every point a of their m-fold meet locus there is a chart, an snc chart of the whole family G at a, adapted to the locus with the m coordinates of the p-members through a as its block.

theorem Manifold.HypersurfaceFamily.IsSnc.isClosedSubmanifold_meetLocus_subfamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {G : HypersurfaceFamily M} {p : G.ι → Prop} (hG : IsSnc ψ G) {m : ℕ} (hm : (G.subfamily p).meetLocus (m + 1) = ∅) : IsClosedSubmanifold ψ ((G.subfamily p).meetLocus m) m

Subfamily form: the m-fold meet locus of the p-members is a closed submanifold of codimension m where no point lies on m + 1 of them.

theorem Manifold.HypersurfaceFamily.IsSnc.hasSncWith_meetLocus_subfamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {G : HypersurfaceFamily M} {p : G.ι → Prop} (hG : IsSnc ψ G) {m : ℕ} (hm : (G.subfamily p).meetLocus (m + 1) = ∅) : HasSncWith ψ G ((G.subfamily p).meetLocus m) m

The whole family G has simple normal crossings with the m-fold meet locus of its p-members where no point lies on m + 1 of them (the centre condition of [Kol07, Definition 66 (3)] at a disjoining step of [Kol07, 72]).