The initial-form map from the Rees algebra of the centre to 𝒪(L)[u]

For I = (x_0, …, x_{r-1}) ⊆ A[x] (r ≤ n) and 𝒪(L) = A[x]/I, the graded ring homomorphism Φ : R̃ = ⊕ I^k t^k → 𝒪(L)[u_0, …, u_{r-1}], c t^k ↦ in_k(c): the degree-k homogeneous component (the initial form) of the image of c ∈ I^k under A[x] ≃ 𝒪(L)[u] (centerSplitEquiv, Hironaka.Scheme.BlowUp.CoordinateSubspace.Split). It is additive, and multiplicative because initial forms multiply (homogeneousComponent_mul_of_mem); it sends x_j t ↦ u_j, constants c ∈ A[x] to c̄, it is surjective in each degree, and its kernel in degree k is I^{k+1} t^k — so it is the identification R̃/I·R̃ = ⊕ I^k/I^{k+1} ≅ 𝒪(L)[u] of the associated graded ring of the coordinate ideal with the polynomial ring ([Mat89, Theorem 16.2] for this monomial case). Proj of it is the closed immersion ℙ^{r-1}_L ⟶ B onto the exceptional divisor (Hironaka.Scheme.BlowUp.CoordinateSubspace.ExceptionalProj).

noncomputable def AlgebraicGeometry.CoordinateSubspace.initialAux (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : Polynomial (MvPolynomial (Fin n) A) →+ MvPolynomial (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)

The initial-form map on polynomials in t: ∑ c_k t^k ↦ ∑ in_k(c_k).

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.initialAux_monomial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (k : ℕ) (c : MvPolynomial (Fin n) A) : (initialAux A n r hrn) ((Polynomial.monomial k) c) = (MvPolynomial.homogeneousComponent k) ((centerSplitEquiv A n r hrn) c)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.genXOfFin (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (j : Fin r) : ↥(centerIdeal A n r)

The variable u_j of 𝒪(L)[u], j : Fin r, as the generator x_j of the center.

Equations

• AlgebraicGeometry.CoordinateSubspace.genXOfFin A n r hrn j = ⟨MvPolynomial.X ⟨↑j, ⋯⟩, ⋯⟩

noncomputable def AlgebraicGeometry.CoordinateSubspace.reesPresentation (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : MvPolynomial (Fin r) (MvPolynomial (Fin n) A) →ₐ[MvPolynomial (Fin n) A] ↥(reesAlgebra (centerIdeal A n r))

The presentation of the Rees algebra: A[x][u_0, …, u_{r-1}] → R̃, u_j ↦ x_j t.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.genMonomial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (j : Fin r) : Polynomial (MvPolynomial (Fin n) A)

The generators of the presentation, in the ambient polynomial ring: x_j t = C x_j · t.

Equations

• AlgebraicGeometry.CoordinateSubspace.genMonomial A n r hrn j = Polynomial.C (MvPolynomial.X ⟨↑j, ⋯⟩) * Polynomial.X

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.ambientPresentation (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : MvPolynomial (Fin r) (MvPolynomial (Fin n) A) →ₐ[MvPolynomial (Fin n) A] Polynomial (MvPolynomial (Fin n) A)

The presentation followed by the inclusion of the Rees algebra into A[x][t].

Equations

• AlgebraicGeometry.CoordinateSubspace.ambientPresentation A n r hrn = MvPolynomial.aeval (AlgebraicGeometry.CoordinateSubspace.genMonomial A n r hrn)

theorem AlgebraicGeometry.CoordinateSubspace.val_comp_reesPresentation (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : (reesAlgebra (centerIdeal A n r)).val.comp (reesPresentation A n r hrn) = ambientPresentation A n r hrn

theorem AlgebraicGeometry.CoordinateSubspace.coe_reesPresentation (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (F : MvPolynomial (Fin r) (MvPolynomial (Fin n) A)) : ↑((reesPresentation A n r hrn) F) = (ambientPresentation A n r hrn) F

theorem AlgebraicGeometry.CoordinateSubspace.reesPresentation_surjective (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : Function.Surjective ⇑(reesPresentation A n r hrn)

The presentation is onto: the Rees algebra is generated over A[x] by the x_j t.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CoordinateSubspace.coeffQuotient (A : Type u) [CommRing A] (n r : ℕ) : MvPolynomial (Fin r) (MvPolynomial (Fin n) A) →+* MvPolynomial (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)

The coefficient map A[x][u] → 𝒪(L)[u].

Equations

• AlgebraicGeometry.CoordinateSubspace.coeffQuotient A n r = MvPolynomial.map (Ideal.Quotient.mk (AlgebraicGeometry.CoordinateSubspace.centerIdeal A n r))

theorem AlgebraicGeometry.CoordinateSubspace.centerSplitEquiv_prod_X_pow (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (β : Fin r →₀ ℕ) : (centerSplitEquiv A n r hrn) (∏ j ∈ β.support, MvPolynomial.X ⟨↑j, ⋯⟩ ^ β j) = (MvPolynomial.monomial β) 1

x^β ↦ u^β under centerSplitEquiv.

theorem AlgebraicGeometry.CoordinateSubspace.initialAux_coe_reesPresentation (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (F : MvPolynomial (Fin r) (MvPolynomial (Fin n) A)) : (initialAux A n r hrn) ↑((reesPresentation A n r hrn) F) = (coeffQuotient A n r) F

The key identity: the initial form of the image of F in the Rees algebra is the reduction of the coefficients of F modulo I.

noncomputable def AlgebraicGeometry.CoordinateSubspace.reesInitial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : ↥(reesAlgebra (centerIdeal A n r)) →+* MvPolynomial (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)

The initial-form ring homomorphism Φ : R̃ → 𝒪(L)[u], c t^k ↦ in_k(c), defined through the presentation A[x][u] → R̃: it is A[x][u] → 𝒪(L)[u] (reduction of the coefficients) on the quotient of A[x][u] by the kernel of the presentation.

Equations

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

theorem AlgebraicGeometry.CoordinateSubspace.reesInitial_apply (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (p : ↥(reesAlgebra (centerIdeal A n r))) : (reesInitial A n r hrn) p = (initialAux A n r hrn) ↑p

theorem AlgebraicGeometry.CoordinateSubspace.reesInitial_mk_monomial (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {k : ℕ} {c : MvPolynomial (Fin n) A} (hc : c ∈ centerIdeal A n r ^ k) : (reesInitial A n r hrn) ⟨(Polynomial.monomial k) c, ⋯⟩ = (MvPolynomial.homogeneousComponent k) ((centerSplitEquiv A n r hrn) c)

theorem AlgebraicGeometry.CoordinateSubspace.reesInitial_mem (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {k : ℕ} {p : ↥(reesAlgebra (centerIdeal A n r))} (hp : p ∈ reesAlgebra.grading (centerIdeal A n r) k) : (reesInitial A n r hrn) p ∈ MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) k

Φ is graded.

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

Φ as a graded ring homomorphism R̃ →+*ᵍ 𝒪(L)[u].

Equations

• AlgebraicGeometry.CoordinateSubspace.reesInitialGraded A n r hrn = { toRingHom := AlgebraicGeometry.CoordinateSubspace.reesInitial A n r hrn, map_mem := ⋯ }

theorem AlgebraicGeometry.CoordinateSubspace.coe_reesInitialGraded (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : ⇑(reesInitialGraded A n r hrn) = ⇑(reesInitial A n r hrn)

theorem AlgebraicGeometry.CoordinateSubspace.reesInitial_degreeOne_genX (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (j : Fin n) (hj : ↑j < r) : (reesInitial A n r hrn) ((reesAlgebra.degreeOne (centerIdeal A n r)) ⟨MvPolynomial.X j, ⋯⟩) = MvPolynomial.X ⟨↑j, hj⟩

Φ (x_j t) = u_j.

theorem AlgebraicGeometry.CoordinateSubspace.reesInitial_algebraMap (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) (c : MvPolynomial (Fin n) A) : (reesInitial A n r hrn) ((algebraMap (MvPolynomial (Fin n) A) ↥(reesAlgebra (centerIdeal A n r))) c) = MvPolynomial.C ((Ideal.Quotient.mk (centerIdeal A n r)) c)

Φ on the constants: c ↦ c̄.

theorem AlgebraicGeometry.CoordinateSubspace.exists_reesInitial_eq (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {k : ℕ} {F : MvPolynomial (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)} (hF : F ∈ MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r) k) : ∃ p ∈ reesAlgebra.grading (centerIdeal A n r) k, (reesInitial A n r hrn) p = F

Φ is surjective in each degree: a homogeneous F of degree k is the image of the monomial c t^k, c the preimage of F under centerSplitEquiv (which lies in I^k).

theorem AlgebraicGeometry.CoordinateSubspace.irrelevant_le_map_reesInitialGraded (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) : HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin r) (MvPolynomial (Fin n) A ⧸ centerIdeal A n r)) ≤ HomogeneousIdeal.map (reesInitialGraded A n r hrn) (HomogeneousIdeal.irrelevant (reesAlgebra.grading (centerIdeal A n r)))

The hypothesis of Proj.map: the irrelevant ideal of 𝒪(L)[u] is contained in the image of the irrelevant ideal of R̃.

theorem AlgebraicGeometry.CoordinateSubspace.reesInitial_mk_monomial_eq_zero_iff (A : Type u) [CommRing A] (n r : ℕ) (hrn : r ≤ n) {k : ℕ} {c : MvPolynomial (Fin n) A} (hc : c ∈ centerIdeal A n r ^ k) : (reesInitial A n r hrn) ⟨(Polynomial.monomial k) c, ⋯⟩ = 0 ↔ c ∈ centerIdeal A n r ^ (k + 1)

The kernel of Φ in degree k: Φ (c t^k) = 0 iff c ∈ I^{k+1} (for c ∈ I^k).