Hironaka's J(m): K_m.comap b = J' · E^m for m large

For X Noetherian there is m₀ such that for all m ≥ m₀ the inverse image of Hironaka's descended centre K_m = I^m ⊓ (J' · E^m).map b along the blow-up map is J' · E^m (exists_comap_descendCenter_eq): the existence of the coherent ideal J(m) with f₀⁻¹(J(m)) = f₀⁻¹(J₀)^m J₁ [Hir64, Ch. 0, §3, p. 133]; [TSPA, Tag 080B]. The inequality ≤ is the Galois connection (comap_descendCenter_le); ≥ is checked on the charts of finitely many affine opens U of X (quasi-compactness) and finitely many generators c of each I(U) (Noetherian), where it is the chart-level inequality of Hironaka.Scheme.BlowUp.Composite.Bound with m ≥ m₀(U, c), and m₀ is the maximum of the finitely many m₀(U, c). The intrinsic definition of K_m needs no gluing of local pieces. Hironaka.Scheme.BlowUp.Composite.Iso turns the equality into the isomorphism of blow-ups.

theorem AlgebraicGeometry.exists_finset_affineOpens_iSup_eq_top {X : Scheme} [CompactSpace ↥X] : ∃ (𝒰 : Finset ↑X.affineOpens), ⨆ U ∈ 𝒰, ↑U = ⊤

A quasi-compact scheme is covered by finitely many affine opens.

theorem AlgebraicGeometry.exists_finset_span_eq {X : Scheme} [IsLocallyNoetherian X] (I : X.IdealSheafData) (U : ↑X.affineOpens) : ∃ (s : Finset ↥(I.ideal U)), Ideal.span (Subtype.val '' ↑s) = I.ideal U

A finite generating set of an ideal of Γ(X, U), X locally Noetherian, as a finite set of elements of the ideal.

theorem AlgebraicGeometry.mem_ideal_chartOpen_iff {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (c : ↥(I.ideal U)) (L : I.blowUp.IdealSheafData) (w : ↑(I.blowUp.presheaf.obj (Opposite.op ↑(chartOpen I U c)))) : w ∈ L.ideal (chartOpen I U c) ↔ (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appIso (Scheme.IdealSheafData.blowUp.chart I U c) ⊤).hom) w ∈ (L.comap (Scheme.IdealSheafData.blowUp.chart I U c)).ideal ⟨⊤, ⋯⟩

Membership in L(chart c ''ᵁ ⊤), read on the affine open ⊤ of the chart.

theorem AlgebraicGeometry.ideal_chartOpen_le_of_comap_le {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) (c : ↥(I.ideal U)) {L L' : I.blowUp.IdealSheafData} (h : L.comap (Scheme.IdealSheafData.blowUp.chart I U c) ≤ L'.comap (Scheme.IdealSheafData.blowUp.chart I U c)) : L.ideal (chartOpen I U c) ≤ L'.ideal (chartOpen I U c)

An inequality of ideal sheaves on the blow-up, pulled back along the chart of c, gives the inequality of their ideals on the affine open chart c ''ᵁ ⊤.

theorem AlgebraicGeometry.comap_chart_le_of_ideal_le {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (U : ↑X.affineOpens) (c : ↥(I.ideal U)) (m : ℕ) (h : chartIdeal I J' U c * Ideal.span {(algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(affineBlowUpAlgebra (I.ideal U) ↑c)) ↑c} ^ m ≤ Ideal.map (algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↥(affineBlowUpAlgebra (I.ideal U) ↑c)) ((descendCenter I J' m).ideal U)) : (J' * I.exceptionalDivisor ^ m).comap (Scheme.IdealSheafData.blowUp.chart I U c) ≤ ((descendCenter I J' m).comap I.blowUpπ).comap (Scheme.IdealSheafData.blowUp.chart I U c)

The chart-level inequality of Hironaka.Scheme.BlowUp.Composite.Bound as an inequality of the pulled-back ideal sheaves.

theorem AlgebraicGeometry.exists_comap_descendCenter_eq {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) [IsNoetherian X] : ∃ (m₀ : ℕ), ∀ (m : ℕ), m₀ ≤ m → (descendCenter I J' m).comap I.blowUpπ = J' * I.exceptionalDivisor ^ m

Hironaka's J(m) [Hir64, Ch. 0, §3, p. 133]; [TSPA, Tag 080B]: for X Noetherian there is m₀ such that for all m ≥ m₀, K_m.comap b = J' · E^m.