The monomial predicate along the assembly of the value

BlowUpSequence.PullbackIsMonomialAtLast L F I: at every point x of the last stage of L, the pull-back of I along the composite blow-down is a monomial in the vanishing ideals of finitely many members of the final total transform of F through x — the chart-free monomial clause of Kollár's explicit formula [Kol07, 72], as a predicate on a list of centres. It is transported along the constructions that assemble the principalization:

• cons (pullbackIsMonomialAtLast_cons): the head blow-up pulls I and F back, the tail carries the predicate (cons_totalTransformSeqFrom_last, stageMapAux_cons_succ);
• concat (pullbackIsMonomialAtLast_concat, by induction through cons): the predicate for the appended list with the boundary and the pulled-back ideal at the junction gives it for the concatenation — the shrink-and-append step is a concat of a pulled-back list;
• eraseEmpty (pullbackIsMonomialAtLast_eraseEmpty): along the diffeomorphism eraseEmptyLast of the last stages (the deletion of the empty blow-ups, [Kol07, 32]) the composites agree (stageMap_last_eraseEmptyLast), the boundary members correspond with the members of the list's boundary outside the range of the empty ones (boundaryCorr_eraseEmpty), and the vanishing ideals transport along the bijective germ map (vanishingStalk_preimage_diffeomorph);
• the order clause ord I_r < 1 of the input ([Kol07, Theorem 107 (1)]) along the pull-back of a list by a local isomorphism (ord_markedTransformSeq_pullback_last_lt_one, via markedTransformSeqAux_pullback): ord < 1 is "the stalk is the unit ideal", which pulls back.

Used for the monomial clause at general mark (MonomialSeqMark.lean).

theorem Manifold.IdealSheaf.ord_lt_one_iff_stalkIdeal_eq_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (x : M.carrier) : ord J x < ↑1 ↔ stalkIdeal J x = ⊤

Order < 1 at a point means the stalk is the unit ideal (ord_eq_zero_iff).

theorem Manifold.IdealSheaf.ord_comap_lt_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (J : M.IdealSheaf) {x : N.carrier} (h : ord J (f x) < ↑1) : (pullback ⇑f ⋯ J).ord x < ↑1

Order < 1 pulls back along any analytic map (the unit stalk maps to the unit ideal).

def AnalyticManifold.BlowUpSequence.PullbackIsMonomialAtLast {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ X) (F : Manifold.HypersurfaceFamily X.carrier) (I : X.IdealSheaf) : Prop

The chart-free reading of Kollár's formula [Kol07, 72] as a predicate on a list: at every point x of the last stage, the pull-back of I along the composite blow-down is a monomial in the vanishing ideals of finitely many members of the final total transform of F through x.

Equations

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

theorem AnalyticManifold.BlowUpSequence.comap_stageMap_last_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (R : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (I : M.IdealSheaf) : Manifold.IdealSheaf.pullback ⇑((cons hY R).toSuccession.stageMap (Fin.last (cons hY R).toSuccession.length)) ⋯ I = Manifold.IdealSheaf.pullback ⇑(R.toSuccession.stageMap (Fin.last R.toSuccession.length)) ⋯ (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hY) ⋯ I)

The composite blow-down of cons hY rest is the head blow-up after the tail's composite, as ideal-sheaf pull-backs.

theorem AnalyticManifold.BlowUpSequence.pullbackIsMonomialAtLast_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (R : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (F : Manifold.HypersurfaceFamily M.carrier) (I : M.IdealSheaf) (hR : R.PullbackIsMonomialAtLast (Manifold.HypersurfaceFamily.totalTransform (⇑(Manifold.blowUpπ ψ₀ hY)) Y F) (Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hY) ⋯ I)) : (cons hY R).PullbackIsMonomialAtLast F I

The predicate for cons hY rest from the predicate for the tail with the pulled-back boundary and ideal.

theorem AnalyticManifold.BlowUpSequence.pullbackIsMonomialAtLast_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (A : BlowUpSequence ψ₀ M) (B : BlowUpSequence ψ₀ (A.stage (Fin.last A.length))) (F : Manifold.HypersurfaceFamily M.carrier) (I : M.IdealSheaf) : B.PullbackIsMonomialAtLast (A.toSuccession.totalTransformSeqFrom F (Fin.last A.toSuccession.length)) (Manifold.IdealSheaf.pullback ⇑(A.toSuccession.stageMap (Fin.last A.toSuccession.length)) ⋯ I) → (A.concat B).PullbackIsMonomialAtLast F I

The predicate for a concatenation from the predicate for the appended list with the boundary and the pulled-back ideal at the junction.

theorem AnalyticManifold.BlowUpSequence.pullbackIsMonomialAtLast_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {F : Manifold.HypersurfaceFamily M.carrier} (hF : ∀ (j : F.ι), IsClosed (F.hyp j)) (I : M.IdealSheaf) (hL : L.PullbackIsMonomialAtLast F I) : L.eraseEmpty.PullbackIsMonomialAtLast F I

The predicate is preserved by the deletion of the empty blow-ups ([Kol07, 32]): along the diffeomorphism eraseEmptyLast of the last stages the composites agree and the boundary members correspond (boundaryCorr_eraseEmpty), the vanishing ideals transporting along the bijective germ map.

theorem AnalyticManifold.BlowUpSequence.ord_markedTransformSeq_pullback_last_lt_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (I E₀ : M.IdealSheaf) (hge : L.toSuccession.IsOfOrderGe I 1 E₀) (hlt : ∀ (x : (L.stage (Fin.last L.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.markedTransformSeq I 1 (Fin.last L.toSuccession.length)) x < ↑1) (q : ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier) : Manifold.IdealSheaf.ord ((L.pullback h hh).toSuccession.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ I) 1 (Fin.last (L.pullback h hh).toSuccession.length)) q < ↑1

The order clause of [Kol07, Theorem 107 (1)] along the pull-back of a list by a local analytic isomorphism: the last marked transform of the pulled-back list is the pull-back of the last marked transform (markedTransformSeqAux_pullback), so ord < 1 — the unit stalk — pulls back.