Collapsing pairwise disjoint members of a divisor into one

Kollár's remark in the construction of the principalization functor [Kol07, 72]: when the irreducible components of E happen to be disjoint one may "declare that E is a single divisor", the components of a divisor being allowed to be reducible in his (68) — after the disjoining blow-ups, the strict transforms E^0 := π^{-1}_*(E_1 + ⋯ + E_k) become one member, placed first, and the exceptional divisors E^1 < ⋯ < E^{k-1} keep their order. This module defines HypersurfaceFamily.collapse G p, the family in which the members satisfying p are replaced by their union as a single first member, and proves it is a simple normal crossings divisor when those members are pairwise disjoint (no point on two of them, (G.subfamily p).meetLocus 2 = ∅): the union is a closed smooth hypersurface (near each of its points it is the one member through the point), the family stays locally finite, and the snc chart of G at a point serves, the union taking the coordinate of the one p-member through the point. The collapse is applied to the boundary at the last stage of the disjoining list to form the disjoined triple (DisjoinInput.lean).

def Manifold.HypersurfaceFamily.subfamily {M : Type u} (G : HypersurfaceFamily M) (p : G.ι → Prop) : HypersurfaceFamily M

The subfamily of the members satisfying p.

Equations

• G.subfamily p = { ι := { j : G.ι // p j }, countable := ⋯, linearOrder := Subtype.instLinearOrder fun (j : G.ι) => p j, hyp := fun (j : { j : G.ι // p j }) => G.hyp ↑j }

def Manifold.HypersurfaceFamily.collapse {M : Type u} (G : HypersurfaceFamily M) (p : G.ι → Prop) : HypersurfaceFamily M

The family with the members satisfying p collapsed into their union as a single first member (Kollár's E^0 = π^{-1}_*(E_1 + ⋯ + E_k), [Kol07, 72]), the others keeping their order (E^1 < ⋯ < E^{k-1}).

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.HypersurfaceFamily.collapse_hyp_inl {M : Type u} (G : HypersurfaceFamily M) (p : G.ι → Prop) : (G.collapse p).hyp (toLex (Sum.inl PUnit.unit)) = ⋃ (j : { j : G.ι // p j }), G.hyp ↑j

theorem Manifold.HypersurfaceFamily.collapse_hyp_inr {M : Type u} (G : HypersurfaceFamily M) (p : G.ι → Prop) (j : { j : G.ι // ¬p j }) : (G.collapse p).hyp (toLex (Sum.inr j)) = G.hyp ↑j

theorem Manifold.HypersurfaceFamily.collapse_hyp_of_ofLex_eq_inl {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} {k : PUnit.{u + 1} ⊕ₗ { j : G.ι // ¬p j }} {u : PUnit.{u + 1}} (hk : ofLex k = Sum.inl u) : (G.collapse p).hyp k = ⋃ (j : { j : G.ι // p j }), G.hyp ↑j

The collapsed member whose index unlexes to Sum.inl is the union.

theorem Manifold.HypersurfaceFamily.collapse_hyp_of_ofLex_eq_inr {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} {k : PUnit.{u + 1} ⊕ₗ { j : G.ι // ¬p j }} {j : { j : G.ι // ¬p j }} (hk : ofLex k = Sum.inr j) : (G.collapse p).hyp k = G.hyp ↑j

The collapsed member whose index unlexes to Sum.inr j is the original member j.

theorem Manifold.HypersurfaceFamily.support_collapse {M : Type u} (G : HypersurfaceFamily M) (p : G.ι → Prop) : (G.collapse p).support = G.support

The support is unchanged by collapsing.

theorem Manifold.HypersurfaceFamily.eq_of_mem_of_mem_subfamily {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} (hdisj : (G.subfamily p).meetLocus 2 = ∅) {x : M} {j j' : (G.subfamily p).ι} (hj : x ∈ (G.subfamily p).hyp j) (hj' : x ∈ (G.subfamily p).hyp j') : j = j'

Where no point lies on two members satisfying p, a point of their union lies on exactly one of them: the member through it is unique.

theorem Manifold.HypersurfaceFamily.exists_nhds_iUnion_eq_hyp {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [TopologicalSpace M] [ChartedSpace E M] (hG : IsSnc ψ G) (hdisj : (G.subfamily p).meetLocus 2 = ∅) {a : M} (j₀ : { j : G.ι // p j }) (ha : a ∈ G.hyp ↑j₀) : ∃ (V : Set M), IsOpen V ∧ a ∈ V ∧ ∀ x ∈ V, x ∈ ⋃ (j : { j : G.ι // p j }), G.hyp ↑j ↔ x ∈ G.hyp ↑j₀

Near a point a of the union of the p-members, when they are pairwise disjoint, the union coincides with the one member through a.

theorem Manifold.HypersurfaceFamily.isClosedSubmanifold_iUnion_subfamily {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [TopologicalSpace M] [ChartedSpace E M] (hG : IsSnc ψ G) (hdisj : (G.subfamily p).meetLocus 2 = ∅) : IsClosedSubmanifold ψ (⋃ (j : { j : G.ι // p j }), G.hyp ↑j) 1

The union of pairwise disjoint closed smooth hypersurfaces of a locally finite family is a closed smooth hypersurface.

theorem Manifold.HypersurfaceFamily.exists_mem_of_mem_collapse_hyp {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} {a : M} {j₀ : G.ι} (ha₀ : a ∈ G.hyp j₀) {k : PUnit.{u + 1} ⊕ₗ { j : G.ι // ¬p j }} (hk : a ∈ (G.collapse p).hyp k) : ∃ (j : G.ι), a ∈ G.hyp j ∧ ((∃ (u : PUnit.{u + 1}), ofLex k = Sum.inl u) ∧ j = j₀ ∨ ∃ (hj : ¬p j), ofLex k = Sum.inr ⟨j, hj⟩)

The index bookkeeping of the collapsed snc chart at a: every collapsed member through a comes from a member of G through a — the ¬ p member itself, or (for the union) the given p-member j₀ through a.

theorem Manifold.HypersurfaceFamily.exists_mem_of_mem_collapse_hyp_of_notMem {M : Type u} {G : HypersurfaceFamily M} {p : G.ι → Prop} {a : M} (ha : a ∉ ⋃ (j : { j : G.ι // p j }), G.hyp ↑j) {k : PUnit.{u + 1} ⊕ₗ { j : G.ι // ¬p j }} (hk : a ∈ (G.collapse p).hyp k) : ∃ (j : G.ι), a ∈ G.hyp j ∧ ∃ (hj : ¬p j), ofLex k = Sum.inr ⟨j, hj⟩

The same, at a point a off the union: only ¬ p members pass.

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

Collapsing pairwise disjoint members into their union keeps the family a simple normal crossings divisor ([Kol07, 72]): the union is a closed smooth hypersurface (near each of its points it is the one member through the point), the family stays locally finite, and the snc chart of G at a point serves, the collapsed member taking the index of the one p-member through the point.