The disjoined triple

After the disjoining blow-ups of [Kol07, 72] the strict transforms E^0 := π^{-1}_*(E_1 + ⋯ + E_k) are pairwise disjoint and form "a smooth divisor", declared a single member; the exceptional divisors E^1, …, E^{k−1} follow; the ideal sheaf is pulled back along the composite π; and "(X', π^* I, ∑ E^i) satisfies the assumptions of (68)", so BMO_1 is applied to it. This module assembles that triple on the last stage of disjoinList: the boundary is the total transform of F with its original members collapsed into one (disjoinedFamily, snc by isSnc_collapse since the original members are pairwise disjoint, meetLocus_two_disjoinFinal_eq_empty), the ideal sheaf is Π^* 𝓘 (nonzero everywhere, isNonzeroEverywhere_comap_stageMap), and the triple lies in the marked class BMOClass 1: its boundary has finitely many members (one collapsed member and finitely many exceptional divisors, finite_notMem_range_originalIdx), as the marked class at mark 1 requires. The construction is stated first for an arbitrary list L along which the original members become pairwise disjoint (disjoinedTripleOf), because the independence of the shrinking open compares the disjoined triples of two lists (DisjoinedNatural.lean); the value of the principalization functor is assembled from the disjoined triple in Assembly.lean. The Hironaka library has the corresponding construction in Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin.lean.

theorem AnalyticManifold.FiniteSuccession.originalIdx_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : Fin (S.length + 1)) : Function.Injective (S.originalIdx F i)

The index of an original member is injective at every stage (originalIdxAux_injective of OrderReduction/BoundaryEnlarge.lean, indexed by Fin).

The disjoined triple of a general list

noncomputable def Hironaka.Manifold.collapsedFamilyOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : AnalyticManifold.BlowUpSequence ψ₀ M) (F : Manifold.HypersurfaceFamily M.carrier) : Manifold.HypersurfaceFamily (L.stage (Fin.last L.length)).carrier

The collapsed boundary at the last stage of a list L — the total transform of F along L with the original members collapsed into one first member (Kollár's E^0, [Kol07, 72]), the exceptional divisors following. The disjoined boundary is its instance at the disjoining list; the general form is what the independence of the shrinking open compares.

Equations

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

theorem Hironaka.Manifold.finite_collapsedFamilyOf_ι {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : AnalyticManifold.BlowUpSequence ψ₀ M) (F : Manifold.HypersurfaceFamily M.carrier) : Finite (collapsedFamilyOf L F).ι

The collapsed boundary has finitely many members: the collapsed one and the exceptional divisors, one per blow-up (finite_notMem_range_originalIdx).

noncomputable def Hironaka.Manifold.disjoinedTripleOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length))) (hdisj : ((L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).subfamily fun (k : (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).ι) => k ∈ Set.range (L.toSuccession.originalIdx T.F (Fin.last L.toSuccession.length))).meetLocus 2 = ∅) : Manifold.AnalyticTriple ψ₀ (L.stage (Fin.last L.length))

The disjoined triple of a list L along which the original members of T.F become pairwise disjoint with snc total transform — the pull-back of the ideal sheaf along the composite and the collapsed boundary (Kollár's (X', π^* I, ∑ E^i), [Kol07, 72]).

Equations

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

theorem Hironaka.Manifold.disjoinedTripleOf_bmoClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length))) (hdisj : ((L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).subfamily fun (k : (L.toSuccession.totalTransformSeqFrom T.F (Fin.last L.toSuccession.length)).ι) => k ∈ Set.range (L.toSuccession.originalIdx T.F (Fin.last L.toSuccession.length))).meetLocus 2 = ∅) : Manifold.AnalyticTriple.BMOClass 1 (disjoinedTripleOf T L hsnc hdisj)

The disjoined triple of a list lies in the marked class at mark 1 (whose finiteness clause asks for finitely many nonempty members).

The disjoined triple of the disjoining list

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

The disjoined boundary — the total transform of F along the disjoining list at its last stage, with the original members (the pairwise disjoint strict transforms E^0 of [Kol07, 72]) collapsed into one first member, the exceptional divisors E^1 < ⋯ < E^{k−1} following.

Equations

• Hironaka.Manifold.disjoinedFamily m F hF hm = Hironaka.Manifold.collapsedFamilyOf (Hironaka.Manifold.disjoinList m F hF hm) F

theorem Hironaka.Manifold.meetLocus_two_subfamily_original_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (m : ℕ) (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) : (((disjoinList m F hF hm).toSuccession.totalTransformSeqFrom F (Fin.last (disjoinList m F hF hm).toSuccession.length)).subfamily fun (k : ((disjoinList m F hF hm).toSuccession.totalTransformSeqFrom F (Fin.last (disjoinList m F hF hm).toSuccession.length)).ι) => k ∈ Set.range ((disjoinList m F hF hm).toSuccession.originalIdx F (Fin.last (disjoinList m F hF hm).toSuccession.length))).meetLocus 2 = ∅

The original members of the final total transform are pairwise disjoint ("we get rid of all pairwise intersections", [Kol07, 72]) — they are disjoinFinal's members (hyp_originalIdx, hyp_disjoinFinal).

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

The disjoined boundary is a simple normal crossings divisor (isSnc_collapse).

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

The disjoined boundary has finitely many members: the collapsed one and the exceptional divisors, one per disjoining blow-up.

noncomputable def Hironaka.Manifold.disjoinedTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {m : ℕ} (hm : T.F.meetLocus (m + 1) = ∅) : Manifold.AnalyticTriple ψ₀ ((disjoinList m T.F ⋯ hm).stage (Fin.last (disjoinList m T.F ⋯ hm).length))

The disjoined triple on the last stage of the disjoining list — the pull-back of the ideal sheaf along the composite and the disjoined boundary (disjoinedTripleOf at the disjoining list); Kollár's (X', π^* I, ∑ E^i), to which BMO_1 is applied [Kol07, 72].

Equations

• Hironaka.Manifold.disjoinedTriple T hm = Hironaka.Manifold.disjoinedTripleOf T (Hironaka.Manifold.disjoinList m T.F ⋯ hm) ⋯ ⋯

theorem Hironaka.Manifold.disjoinedTriple_bmoClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {m : ℕ} (hm : T.F.meetLocus (m + 1) = ∅) : Manifold.AnalyticTriple.BMOClass 1 (disjoinedTriple T hm)

The disjoined triple lies in the marked class at mark 1 (whose finiteness clause asks for finitely many nonempty members).