The exceptional divisor of the model blow-up is ℙ^{r-1}_L

Setting: R = A[x_0, …, x_{n-1}], I = (x_0, …, x_{r-1}) with r ≤ n, 𝒪(L) = R/I, B = Proj R̃ the model blow-up with charts U_j = Spec R[I/x_j], and F = V(I·𝒪_B) the exceptional divisor. Hironaka.Scheme.BlowUp.CoordinateSubspace.ReesInitial built the graded ring homomorphism Φ : R̃ →+*ᵍ 𝒪(L)[u_0, …, u_{r-1}], c t^k ↦ in_k(c), surjective in every degree with kernel I·R̃. This module takes Proj of it (Mathlib's Proj.map) and shows that g = Proj Φ : ℙ^{r-1}_L ⟶ B is a closed immersion with kernel the exceptional ideal, so that F ≅ ℙ^{r-1}_L (exists_iso_exceptional_proj): the exceptional divisor of a blow-up of 𝔸ⁿ is the projective space of directions [Hau14, Definitions 4.8–4.10], as in the point blow-up [Hau14, Example 4.41]. The result is used for the exceptional divisor of a blow-up of a smooth centre as a projective bundle (Hironaka.Scheme.Smooth.ExceptionalBundle).

Everything is checked on the chart cover U_j, j < r, of B:

• On the chart of x_j the map g is Spec of the ring map ψ_j : R[I/x_j] ≅ (R̃_{x_j t})₀ → (𝒪(L)[u]_{u_j})₀, c/x_j^k ↦ in_k(c)/u_j^k (isPullback_chart: the square is a pullback because g⁻¹(U_j) = D₊(u_j), Mathlib's Proj.awayι_comp_map and Proj.map_preimage_basicOpen).
• ψ_j is surjective (in_k is surjective onto the forms of degree k) and its kernel is x_j·R[I/x_j]: in_k(c) = 0 iff c ∈ I^{k+1} (reesInitial_mk_monomial_eq_zero_iff), i.e. iff c/x_j^k = x_j · c/x_j^{k+1} (ker_chartInitialMap, ker_chartQuotientMap); here u_j is a nonzerodivisor of the polynomial ring, so F/u_j^k = 0 iff F = 0 (HomogeneousLocalization.Away.mk_eq_zero_iff_of_isRegular).
• Hence g is a closed immersion (local on the target; Spec of a surjection), and its kernel agrees on every U_j with the exceptional ideal, which on U_j is x_j·R[I/x_j] (affineBlowUp.comap_exceptionalIdeal_chart). Ideal sheaves agreeing on an affine cover agree (le_of_iSup_eq_top), so g.ker = I·𝒪_B (ker_projInitial).
• Two closed immersions with the same kernel are isomorphic over B (IsClosedImmersion.isIso_lift); the chart condition is g⁻¹(U_j) = D₊(u_j) and the compatibility with the projections is Proj.map_toSpecZero (Hironaka.Scheme.BlowUp.Rees.Map) together with Φ(c) = c̄ on constants.

theorem HomogeneousLocalization.Away.mk_eq_zero_iff_of_isRegular {σ : Type u_1} {A : Type u_2} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (hreg : IsRegular f) (k : ℕ) (x : A) (hx : x ∈ 𝒜 (k • d)) : Away.mk 𝒜 hf k x hx = 0 ↔ x = 0

A fraction x / f ^ k in the homogeneous localization away from a nonzerodivisor f is zero iff x = 0.

The chart of x_j: the ring map R[I/x_j] → (𝒪(L)[u]_{u_j})₀

noncomputable def AlgebraicGeometry.CoordinateSubspace.chartInitialMap (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : HomogeneousLocalization.Away (reesAlgebra.grading (centerIdeal A n r)) ((reesAlgebra.degreeOne (centerIdeal A n r)) a) →+* HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ((reesInitialGraded A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) a))

The initial-form map on the chart ring of a t: (R̃_{a t})₀ → (𝒪(L)[u]_{Φ(a t)})₀, c t^k / (a t)^k ↦ in_k(c) / Φ(a t)^k.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.chartInitialMap_surjective (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : Function.Surjective ⇑(chartInitialMap A n r hrn a)

The initial-form map on the chart of a is surjective: every form of degree k is the initial form of an element of I^k t^k.

noncomputable def AlgebraicGeometry.CoordinateSubspace.chartQuotientMap (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : ↥(affineBlowUpAlgebra (centerIdeal A n r) ↑a) →+* HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ((reesInitialGraded A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) a))

The initial-form map read on R[I/a] ≅ (R̃_{a t})₀: c/a^k ↦ in_k(c)/Φ(a t)^k.

Equations

• AlgebraicGeometry.CoordinateSubspace.chartQuotientMap A n r hrn a = (AlgebraicGeometry.CoordinateSubspace.chartInitialMap A n r hrn a).comp (reesAlgebra.chartRingEquiv a).symm.toRingHom

theorem AlgebraicGeometry.CoordinateSubspace.chartQuotientMap_surjective (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : Function.Surjective ⇑(chartQuotientMap A n r hrn a)

theorem AlgebraicGeometry.CoordinateSubspace.isRegular_reesInitialGraded_degreeOne (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) (j : Fin n) (hj : ↑j < r) (ha : ↑a = MvPolynomial.X j) : _root_.IsRegular ((reesInitialGraded A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) a))

Φ(x_j t) = u_j is a nonzerodivisor.

theorem AlgebraicGeometry.CoordinateSubspace.ker_chartInitialMap (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) (j : Fin n) (hj : ↑j < r) (ha : ↑a = MvPolynomial.X j) : RingHom.ker (chartInitialMap A n r hrn a) = Ideal.span {(HomogeneousLocalization.fromZeroRingHom (reesAlgebra.grading (centerIdeal A n r)) (Submonoid.powers ((reesAlgebra.degreeOne (centerIdeal A n r)) a))) ((reesAlgebra.gradingZeroEquiv (centerIdeal A n r)).symm ↑a)}

The kernel on the chart of x_j: in_k(c)/u_j^k = 0 iff c ∈ I^{k+1} iff c t^k/(x_j t)^k is a multiple of x_j/1.

theorem AlgebraicGeometry.CoordinateSubspace.ker_chartQuotientMap (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) (j : Fin n) (hj : ↑j < r) (ha : ↑a = MvPolynomial.X j) : RingHom.ker (chartQuotientMap A n r hrn a) = Ideal.span {(algebraMap (MvPolynomial (Fin n) A) ↥(affineBlowUpAlgebra (centerIdeal A n r) ↑a)) ↑a}

On the chart U_j = Spec R[I/x_j] the kernel of the initial-form map is x_j · R[I/x_j].

Proj of the initial-form map

noncomputable def AlgebraicGeometry.CoordinateSubspace.projInitial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : Proj (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ⟶ modelBlowUp A n r

The morphism ℙ^{r-1}_L = Proj 𝒪(L)[u] ⟶ B = Proj R̃, Proj of the initial-form map Φ (Mathlib's Proj.map).

Equations

• AlgebraicGeometry.CoordinateSubspace.projInitial A n r hrn = AlgebraicGeometry.Proj.map (AlgebraicGeometry.CoordinateSubspace.reesInitialGraded A n r hrn) ⋯

theorem AlgebraicGeometry.CoordinateSubspace.awayι_projInitial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : CategoryTheory.CategoryStruct.comp (Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ((reesInitialGraded A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) a)) ⋯ ⋯) (projInitial A n r hrn) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (chartQuotientMap A n r hrn a))) (affineBlowUp.chart (centerIdeal A n r) a)

The chart square: on D₊(Φ(a t)) the morphism Proj Φ is Spec of the chart-ring map.

theorem AlgebraicGeometry.CoordinateSubspace.projInitial_preimage_opensRange_chart (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : (TopologicalSpace.Opens.map (projInitial A n r hrn).base).obj (Scheme.Hom.opensRange (affineBlowUp.chart (centerIdeal A n r) a)) = Scheme.Hom.opensRange (Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ((reesInitialGraded A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) a)) ⋯ ⋯)

(Proj Φ)⁻¹(U_a) = D₊(Φ(a t)).

theorem AlgebraicGeometry.CoordinateSubspace.isPullback_chart (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : CategoryTheory.IsPullback (Spec.map (CommRingCat.ofHom (chartQuotientMap A n r hrn a))) (Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ((reesInitialGraded A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) a)) ⋯ ⋯) (affineBlowUp.chart (centerIdeal A n r) a) (projInitial A n r hrn)

The chart square is a pullback square.

theorem AlgebraicGeometry.CoordinateSubspace.isClosedImmersion_pullback_snd_chart (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) : IsClosedImmersion (CategoryTheory.Limits.pullback.snd (projInitial A n r hrn) (affineBlowUp.chart (centerIdeal A n r) a))

The pullback of Proj Φ to the chart of a is a closed immersion.

instance AlgebraicGeometry.CoordinateSubspace.isClosedImmersion_projInitial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : IsClosedImmersion (projInitial A n r hrn)

Proj Φ : ℙ^{r-1}_L ⟶ B is a closed immersion — it is one over every chart U_j, j < r, where it is Spec of the surjection R[I/x_j] → (𝒪(L)[u]_{u_j})₀.

theorem AlgebraicGeometry.CoordinateSubspace.ideal_comap_ker_projInitial_chart_top (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) (j : Fin n) (hj : ↑j < r) (ha : ↑a = MvPolynomial.X j) : ((Scheme.Hom.ker (projInitial A n r hrn)).comap (affineBlowUp.chart (centerIdeal A n r) a)).ideal ⟨⊤, ⋯⟩ = Ideal.span {affineBlowUp.chartGenerator (centerIdeal A n r) a}

On the chart of x_j, the kernel of Proj Φ pulls back to the ideal x_j · R[I/x_j] (ker_chartQuotientMap through the pullback square) — the same ideal as the exceptional ideal (affineBlowUp.ideal_comap_exceptionalIdeal_chart_top).

theorem AlgebraicGeometry.CoordinateSubspace.ker_projInitial_ideal_image_chart (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (a : ↥(centerIdeal A n r)) (j : Fin n) (hj : ↑j < r) (ha : ↑a = MvPolynomial.X j) : (Scheme.Hom.ker (projInitial A n r hrn)).ideal ⟨(Scheme.Hom.opensFunctor (affineBlowUp.chart (centerIdeal A n r) a)).obj ⊤, ⋯⟩ = (affineBlowUp.exceptionalIdeal (centerIdeal A n r)).ideal ⟨(Scheme.Hom.opensFunctor (affineBlowUp.chart (centerIdeal A n r) a)).obj ⊤, ⋯⟩

The same on the sections over the image of the chart, U_j = chart ''ᵁ ⊤: the kernel of Proj Φ and the exceptional ideal agree there.

theorem AlgebraicGeometry.CoordinateSubspace.ker_projInitial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : Scheme.Hom.ker (projInitial A n r hrn) = affineBlowUp.exceptionalIdeal (centerIdeal A n r)

The kernel of Proj Φ : ℙ^{r-1}_L ⟶ B is the exceptional ideal I·𝒪_B — the two ideal sheaves agree on the affine cover by the charts U_j, j < r.

theorem AlgebraicGeometry.CoordinateSubspace.projInitial_π (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : CategoryTheory.CategoryStruct.comp (projInitial A n r hrn) (affineBlowUp.π (centerIdeal A n r)) = CategoryTheory.CategoryStruct.comp (Proj.toSpecZero (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r))) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) ↥(MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) 0)))) (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (centerIdeal A n r)))))

The compatibility with the projections: Proj Φ followed by the blow-up map π : B ⟶ Spec R is the structure map ℙ^{r-1}_L ⟶ L = Spec 𝒪(L) followed by L ⟶ Spec R (Proj.map_toSpecZero, and Φ(c) = c̄ on constants).

theorem AlgebraicGeometry.CoordinateSubspace.exists_iso_exceptional_proj (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : ∃ (e : (affineBlowUp.exceptionalIdeal (centerIdeal A n r)).subscheme ≅ Proj (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r))), (∀ (j : Fin n) (hj : ↑j < r), (Scheme.Hom.opensFunctor e.hom).obj ((TopologicalSpace.Opens.map (affineBlowUp.exceptionalIdeal (centerIdeal A n r)).subschemeι.base).obj (Scheme.Hom.opensRange (modelChart A n r j hj))) = Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) (MvPolynomial.X ⟨↑j, hj⟩)) ∧ CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp (affineBlowUp.exceptionalIdeal (centerIdeal A n r)).subschemeι (affineBlowUp.π (centerIdeal A n r))) = CategoryTheory.CategoryStruct.comp (Proj.toSpecZero (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r))) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) ↥(MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) 0)))) (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (centerIdeal A n r)))))

The exceptional divisor F = V(I·𝒪_B) of the model blow-up is ℙ^{r-1}_L [Hau14, Definitions 4.8–4.10]; [Hau14, Example 4.41]: an isomorphism F ≅ Proj 𝒪(L)[u_0, …, u_{r-1}] under which the piece of F in the chart U_j is D₊(u_j) and which is compatible with the structure maps to L and Spec R. The isomorphism is the lift of the closed immersion Proj Φ through F ⟶ B, an isomorphism because the two closed immersions have the same kernel.