Enlarging the boundary by members missing the cosupport

After Step 2.1 of the proof of [Kol07, Theorem 103], "cosupp(I_r, m) is disjoint from Π^{-1}_* E" ([Kol07, 104, Step 2.1.j]), so Step 2.2 may run with the boundary consisting of the exceptional divisors and the transform H_r of the hypersurface of maximal contact, while the sequence is of order ≥ m for the full transformed boundary as well: the extra members, the transforms of the original members of E, miss every centre, and a member missing the centre is invisible to the normal-crossings condition at the points of the centre ([Kol07, Definition 24], whose chart only constrains the members through the point).

The general form, not in the sources: a blow-up sequence of order ≥ m for (𝓘, m, red F) is of order ≥ m for (𝓘, m, red G) whenever every member of G meeting the cosupport {ord 𝓘 ≥ m} is a member of F, injectively (through a map e : G.ι → F.ι). The proof is the joint induction of BoundaryFamily.lean on the stages: at every stage the boundary family from G is the family from F with extra members missing the centre, because a member of G_i through a point of the centre is either the strict transform of a member of G (which then meets the cosupport, the cosupport at stage i lying over the cosupport at the start and the strict transform over the member) or an exceptional divisor, shared by the two families.

• HypersurfaceFamily.HasSncWith.of_forall_mem_exists — simple normal crossings pass to a family whose members through the points of Y are, injectively, members of the first.
• FiniteSuccession.originalIdxAux_or_exceptionalEmb, originalIdxAux_injective, originalIdxAux_ne_exceptionalEmb — every member of the stage-i family is the transform of an original member or an exceptional divisor, and the two kinds are distinct.
• FiniteSuccession.corrIdxAux, corrIdxAux_originalIdxAux, corrIdxAux_exceptionalEmb — the correspondence of index sets at every stage induced by e.
• FiniteSuccession.IsOfOrderGe.of_forall_hyp_eq_of_mem — the enlargement.

The enlargement is applied in Step22FamFull.lean; the index correspondence is reused in Step21Indiff.lean for the indifference to empty boundary members.

theorem Manifold.HypersurfaceFamily.HasSncWith.of_forall_mem_exists {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F G : HypersurfaceFamily M} {Y : Set M} {c : ℕ} (h : HasSncWith ψ F Y c) (e : (a : M) → a ∈ Y → { k : G.ι // a ∈ G.hyp k } → { j : F.ι // a ∈ F.hyp j }) (he_inj : ∀ (a : M) (ha : a ∈ Y), Function.Injective (e a ha)) (he_hyp : ∀ (a : M) (ha : a ∈ Y) (k : { k : G.ι // a ∈ G.hyp k }), G.hyp ↑k = F.hyp ↑(e a ha k)) : HasSncWith ψ G Y c

Simple normal crossings with F pass to a family G whose members through each point a of Y are, injectively, members of F through a with the same hypersurface: the chart of F at a serves, with its coordinate indices transported along the correspondence.

The two kinds of members of the stage-i family

theorem AnalyticManifold.FiniteSuccession.originalIdxAux_or_exceptionalEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : ℕ) (h : i < S.length + 1) (a : (S.totalTransformSeqFromAux F i h).ι) : (∃ (j : F.ι), a = S.originalIdxAux F i h j) ∨ ∃ (k : (S.totalTransformSeqAux i h).ι), a = S.exceptionalEmb F i h k

Every member of the boundary family at stage i is the transform of an original member or an exceptional divisor.

theorem AnalyticManifold.FiniteSuccession.originalIdxAux_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : ℕ) (h : i < S.length + 1) : Function.Injective (S.originalIdxAux F i h)

The transforms of distinct original members are distinct members.

theorem AnalyticManifold.FiniteSuccession.originalIdxAux_ne_exceptionalEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : ℕ) (h : i < S.length + 1) (j : F.ι) (k : (S.totalTransformSeqAux i h).ι) : S.originalIdxAux F i h j ≠ S.exceptionalEmb F i h k

The transform of an original member is never an exceptional divisor.

The correspondence of index sets induced by a map of the starts

def AnalyticManifold.FiniteSuccession.corrIdxAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) (i : ℕ) (h : i < S.length + 1) : (S.totalTransformSeqFromAux G i h).ι → (S.totalTransformSeqFromAux F i h).ι

The map of index sets at stage i induced by a map e : G.ι → F.ι of the starting index sets: transforms of original members along e, exceptional divisors to themselves.

Equations

• S.corrIdxAux e 0 x_2 = e
• S.corrIdxAux e i.succ h = fun (a : (S.totalTransformSeqFromAux G (i + 1) h).ι) => toLex (Sum.map (S.corrIdxAux e i ⋯) id (ofLex a))

theorem AnalyticManifold.FiniteSuccession.corrIdxAux_originalIdxAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) (i : ℕ) (h : i < S.length + 1) (j : G.ι) : S.corrIdxAux e i h (S.originalIdxAux G i h j) = S.originalIdxAux F i h (e j)

theorem AnalyticManifold.FiniteSuccession.corrIdxAux_exceptionalEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) (i : ℕ) (h : i < S.length + 1) (k : (S.totalTransformSeqAux i h).ι) : S.corrIdxAux e i h (S.exceptionalEmb G i h k) = S.exceptionalEmb F i h k

The enlargement

theorem AnalyticManifold.FiniteSuccession.hyp_corrIdxAux_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) [FiniteDimensional 𝕜 E] {J : M.IdealSheaf} {m : ℕ} (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (hge : S.IsOfOrderGe J m F.idealSheaf) (hmem : ∀ (k : G.ι), (∃ a ∈ G.hyp k, ↑m ≤ Manifold.IdealSheaf.ord J a) → G.hyp k = F.hyp (e k)) (i : Fin (S.length + 1)) (a : (S.stage i).carrier) (hord : ↑m ≤ Manifold.IdealSheaf.ord (S.markedTransformSeq J m i) a) (kk : (S.totalTransformSeqFrom G i).ι) (ha : a ∈ (S.totalTransformSeqFrom G i).hyp kk) : (S.totalTransformSeqFrom G i).hyp kk = (S.totalTransformSeqFrom F i).hyp (S.corrIdxAux e ↑i ⋯ kk)

A member of the stage-i family from G through a point of the cosupport of the marked transform is, under the correspondence, a member of the stage-i family from F with the same hypersurface: the transform of an original member, which then meets the cosupport of 𝓘 (the cosupport at stage i lies over the cosupport at the start, le_ord_stageMap, and the strict transform over the member), or an exceptional divisor.

theorem AnalyticManifold.FiniteSuccession.corrIdxAux_injOn_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) [FiniteDimensional 𝕜 E] {J : M.IdealSheaf} {m : ℕ} (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (hge : S.IsOfOrderGe J m F.idealSheaf) (hinj : ∀ (k k' : G.ι), (∃ a ∈ G.hyp k, ↑m ≤ Manifold.IdealSheaf.ord J a) → (∃ a ∈ G.hyp k', ↑m ≤ Manifold.IdealSheaf.ord J a) → e k = e k' → k = k') (i : Fin (S.length + 1)) (a : (S.stage i).carrier) (hord : ↑m ≤ Manifold.IdealSheaf.ord (S.markedTransformSeq J m i) a) (kk kk' : (S.totalTransformSeqFrom G i).ι) (ha : a ∈ (S.totalTransformSeqFrom G i).hyp kk) (ha' : a ∈ (S.totalTransformSeqFrom G i).hyp kk') (heq : S.corrIdxAux e ↑i ⋯ kk = S.corrIdxAux e ↑i ⋯ kk') : kk = kk'

The correspondence is injective on the members through a point of the cosupport of the marked transform.

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.of_forall_hyp_eq_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F G : Manifold.HypersurfaceFamily M.carrier} (e : G.ι → F.ι) [FiniteDimensional 𝕜 E] {J : M.IdealSheaf} {m : ℕ} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hG : Manifold.HypersurfaceFamily.IsSnc ψ G) (hge : S.IsOfOrderGe J m F.idealSheaf) (hmem : ∀ (k : G.ι), (∃ a ∈ G.hyp k, ↑m ≤ Manifold.IdealSheaf.ord J a) → G.hyp k = F.hyp (e k)) (hinj : ∀ (k k' : G.ι), (∃ a ∈ G.hyp k, ↑m ≤ Manifold.IdealSheaf.ord J a) → (∃ a ∈ G.hyp k', ↑m ≤ Manifold.IdealSheaf.ord J a) → e k = e k' → k = k') : S.IsOfOrderGe J m G.idealSheaf

A smooth blow-up sequence of order ≥ m for (𝓘, m, red F) is of order ≥ m for (𝓘, m, red G) when every member of G meeting the cosupport {ord 𝓘 ≥ m} is, injectively, a member of F (the general form of the observation in [Kol07, 104, Step 2.1.j] that the transforms of the original boundary miss the cosupport after Step 2.1). The order clause of [Kol07, Definition 66] does not see the boundary; the normal-crossings clause at every stage follows by the joint induction of BoundaryFamily.lean and HasSncWith.of_forall_mem_exists, the members of the family from G through a point of the centre corresponding to members of the family from F. Not in the sources.