One step of the monomial formula: a boundary monomial pulled back along a blow-up

The intrinsic, chart-free form of Kollár's Π^* I = 𝒪(−∑ Π^*_{r,j+1} F_j) [Kol07, 72] at a point x: J is a boundary monomial at x with residual R — J_x = (∏_{j ∈ s} I(E^j)_x^{α_j}) · R_x for finitely many members E^j of the boundary family through x (HypersurfaceFamily.IsBoundaryMonomialAt). The monomial clause of the principalization is this predicate at the last stage with the unit residual.

isBoundaryMonomialAt_pullback: the form is preserved by one blowing-up π along a centre Y with simple normal crossings with the family, provided the residual is divided exactly by a power of the exceptional ideal (R_{π p} pulls back to I_{F,p}^e · R'_p): each member through π p pulls back to I_{F,p}^ε · I(strict transform)_p (MonomialStalk.lean), the exponents on the exceptional member add up, and the members of the total transform not through p (strict transforms missing p; the exceptional divisor when π p ∉ Y) contribute the unit ideal and are dropped from the index set. The total transform of a divisor is that of [Kol07, Definition 25]; the marked transform with its exact division is [Kol07, (60.1)]. Used stage by stage in MonomialSeq.lean and in the monomial step of the order reduction.

theorem Hironaka.Manifold.Ideal.map_finset_prod {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {ι : Type u_3} (s : Finset ι) (g : ι → Ideal R) : Ideal.map f (∏ i ∈ s, g i) = ∏ i ∈ s, Ideal.map f (g i)

Ideal.map of a finite product of ideals is the product of the images.

def Manifold.HypersurfaceFamily.IsBoundaryMonomialAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : AnalyticManifold 𝕜 E} (G : HypersurfaceFamily X.carrier) (J R : X.IdealSheaf) (x : X.carrier) : Prop

The intrinsic reading of Kollár's explicit formula at a point [Kol07, 72]: J is at x a monomial in the vanishing ideals of finitely many members of G through x, times the residual R — J_x = (∏_{j ∈ s} I(G^j)_x^{α j}) · R_x with x ∈ G^j for j ∈ s.

Equations

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

def Manifold.HypersurfaceFamily.inlTotalEmb {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M M' : AnalyticManifold 𝕜 E} (F : HypersurfaceFamily M.carrier) (π : M'.carrier → M.carrier) (Y : Set M.carrier) : F.ι ↪ (totalTransform π Y F).ι

The strict-transform index j ↦ inl j of the total transform, as an embedding.

Equations

• F.inlTotalEmb π Y = { toFun := fun (j : F.ι) => toLex (Sum.inl j), inj' := ⋯ }

theorem Hironaka.Manifold.isBoundaryMonomialAt_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) {J R : M.IdealSheaf} {R' : M'.IdealSheaf} {p : M'.carrier} (hJ : F.IsBoundaryMonomialAt J R (π p)) {e : ℕ} (hR : Ideal.map (Manifold.germMap π ⋯ p) (Manifold.IdealSheaf.stalkIdeal R (π p)) = Manifold.vanishingStalk (π ⁻¹' Y) p ^ e * Manifold.IdealSheaf.stalkIdeal R' p) : (Manifold.HypersurfaceFamily.totalTransform π Y F).IsBoundaryMonomialAt (Manifold.IdealSheaf.pullback π ⋯ J) R' p

Kollár's formula, one step ([Kol07, 72]; the exact division of [Kol07, (60.1)]): if J is a boundary monomial at π p with residual R, and the residual pulls back to I_{F,p}^e · R'_p, then the pull-back π⁻¹(J) is a boundary monomial at p for the total transform of the family with residual R' — the members through π p pull back to I_F^ε times their strict transforms (exists_map_germMap_vanishingStalk_hyp_eq'), the exceptional exponents add, and the members of the total transform not through p are dropped (their vanishing ideal at p is the unit ideal).