The graded Rees algebra: components and degree one #
Basic facts about the grading reesAlgebra.grading I of the Rees algebra ⨁ᵢ Iⁱ tⁱ
[Hau14, Definition 4.6], in which Mathlib's polynomial variable X plays the role of Hauser's t.
reesAlgebra.coe_component: the degree-ncomponent ofpis the monomial(coeff n p) tⁿ.reesAlgebra.degreeOne I : I →ₗ[R] reesAlgebra I: the degree-one elementa tofa ∈ I[Hau14, Definition 4.16], whose range is the degree-one piece (reesAlgebra.grading_one_eq_range) and whose values generate the irrelevant ideal (Hironaka.Scheme.BlowUp.Rees.Irrelevant).
@[simp]
theorem
reesAlgebra.coe_component
{R : Type u}
[CommRing R]
{I : Ideal R}
(n : ℕ)
(p : ↥(reesAlgebra I))
:
The degree-one element a t of the Rees algebra, for a ∈ I — an element of I defines a
homogeneous element of degree 1 of the Rees algebra [Hau14, Definition 4.16] — as an R-linear
map I → reesAlgebra I. Its range is the degree-one piece (reesAlgebra.grading_one_eq_range),
its values generate the irrelevant ideal (reesAlgebra.irrelevant_le_span_degreeOne), and the
chart cover of the affine blow-up is indexed by it (affineBlowUp.affineOpenCover).
Equations
- reesAlgebra.degreeOne I = { toFun := fun (a : ↥I) => ⟨(Polynomial.monomial 1) ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }