The disjoining list against the running total transform

Clause (1) of [Kol07, Theorem 35] for the disjoining blow-ups of [Kol07, 72]: every centre has simple normal crossings with the current divisor — the TOTAL transform of the boundary so far (the strict transforms of the components of E together with the exceptional divisors), so that the end result (X', π^* I, ∑ E^i) "satisfies the assumptions of (68)" (Kollár's Z_1 "is smooth since the (π_0)^{-1}_* E_i do not have any k-fold intersections"). Clause (1) asks this of every centre of the value against totalTransformSeqFrom (F|U) at its stage, in the given codimension. This module proves it for the disjoining list: carrying along the recursion any snc family G that contains the members of F (an injective relabelling e with G.hyp (e j) = F.hyp j — at the start G = F, e = id; after a step G' = G.totalTransform π Y, e' = toLex ∘ inl ∘ e), the boundary family totalTransformSeqFrom G is snc at every stage and every centre — the meet locus of the F-members, which is the meet locus of the e-subfamily of G — has snc with it (disjoinList_boundary), the given codimension matched by IsClosedSubmanifold.codim_eq_of_nonempty (an empty centre satisfies the clause vacuously; [Kol07, 32]). Used by DisjoinInput.lean (the disjoined boundary is snc) and ClauseOne.lean. The Hironaka library has the corresponding statement in Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin.lean.

theorem Manifold.HypersurfaceFamily.meetLocus_subfamily_range_eq {M : Type u} {G F : HypersurfaceFamily M} (e : F.ι → G.ι) (he : Function.Injective e) (hhyp : ∀ (j : F.ι), G.hyp (e j) = F.hyp j) (k : ℕ) : (G.subfamily fun (g : G.ι) => g ∈ Set.range e).meetLocus k = F.meetLocus k

The meet loci of the subfamily indexed by the range of an injective relabelling with the same members are those of the relabelled family.

theorem Manifold.HypersurfaceFamily.HasSncWith.of_codim {𝕜 : 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} {Y : Set M} {c c' n' : ℕ} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} (h : HasSncWith ψ F Y c) (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ' Y c') : HasSncWith ψ F Y c'

Simple normal crossings with a closed submanifold does not depend on the codimension given for it — for a nonempty Y the codimension is unique (codim_eq_of_nonempty), for an empty Y the clause is vacuous (the empty blow-up convention, [Kol07, 32]).

theorem Hironaka.Manifold.disjoinList_boundary {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) (G : Manifold.HypersurfaceFamily M.carrier) (e : F.ι → G.ι) : Manifold.HypersurfaceFamily.IsSnc ψ₀ G → Function.Injective e → (∀ (j : F.ι), G.hyp (e j) = F.hyp j) → (∀ (i : Fin ((disjoinList m F hF hm).toSuccession.length + 1)), Manifold.HypersurfaceFamily.IsSnc ψ₀ ((disjoinList m F hF hm).toSuccession.totalTransformSeqFrom G i)) ∧ ∀ (i : Fin (disjoinList m F hF hm).toSuccession.length), Manifold.HypersurfaceFamily.HasSncWith ψ₀ ((disjoinList m F hF hm).toSuccession.totalTransformSeqFrom G i.castSucc) (Manifold.IdealSheaf.support ((disjoinList m F hF hm).toSuccession.center i)) ((disjoinList m F hF hm).toSuccession.codim i)

Clause (1) of [Kol07, Theorem 35] for the disjoining blow-ups of [Kol07, 72]: along the disjoining list, for any snc family G containing the members of F (an injective relabelling e with the same members), the boundary family totalTransformSeqFrom G is snc at every stage, and every centre has snc with it at its stage, in the given codimension.

theorem Hironaka.Manifold.disjoinList_center_hasSncWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) (i : Fin (disjoinList m F hF hm).toSuccession.length) : Manifold.HypersurfaceFamily.HasSncWith ψ₀ ((disjoinList m F hF hm).toSuccession.totalTransformSeqFrom F i.castSucc) (Manifold.IdealSheaf.support ((disjoinList m F hF hm).toSuccession.center i)) ((disjoinList m F hF hm).toSuccession.codim i)

Clause (1) of [Kol07, Theorem 35] for the disjoining list from its own family F (e = id).

theorem Hironaka.Manifold.disjoinList_isSnc_totalTransformSeqFrom {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) (i : Fin ((disjoinList m F hF hm).toSuccession.length + 1)) : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((disjoinList m F hF hm).toSuccession.totalTransformSeqFrom F i)

The boundary family from F along the disjoining list is snc at every stage.