Degree zero of the graded Rees algebra, and finite type

The degree-zero piece of reesAlgebra I = ⨁ₙ Iⁿ tⁿ is R itself: R embeds into the Rees algebra by sending g to the degree-zero element g · t⁰ [Hau14, Definition 4.6], and the ring isomorphism reesAlgebra.gradingZeroEquiv I : grading I 0 ≃+* R records that identification. This file proves the constant-map triangle: composing its inverse with the grading-induced structure map algebraMap (grading I 0) (reesAlgebra I) — the map Mathlib's Proj.toSpecZero and HomogeneousLocalization.fromZeroRingHom use — gives algebraMap R (reesAlgebra I).

The triangle is what transports finite type: if I is finitely generated by g₁, …, gₖ then the Rees algebra is R[g₁t, …, gₖt] [Hau14, Definition 4.6] (Mathlib's reesAlgebra.fg), and the same finitely many degree-one generators generate over grading I 0, because the constants R → reesAlgebra I factor through grading I 0 — in Lean, the scalar tower IsScalarTower R (grading I 0) (reesAlgebra I), from which Algebra.FiniteType.of_restrictScalars_finiteType restricts the base. The finite-type statement is for the grading-induced algebra structure on reesAlgebra I over grading I 0, since that is the hypothesis of Mathlib's IsProper (Proj.toSpecZero 𝒜); no unrelated algebra structure is introduced.

Main declarations

• reesAlgebra.gradingZeroEquiv_apply, reesAlgebra.coe_gradingZeroEquiv_symm: the equivalence is p ↦ coeff 0 p, with inverse r ↦ algebraMap R (reesAlgebra I) r.
• reesAlgebra.algebraMap_gradingZeroEquiv_symm: the constant-map triangle.
• reesAlgebra.finiteType_of_fg: I.FG → Algebra.FiniteType (grading I 0) (reesAlgebra I).

Boundary cases

For I = 0 the Rees algebra is its own degree-zero piece and the equivalence is reesAlgebra 0 ≃ R; for the zero ring both sides are singletons. I.FG is used only in finiteType_of_fg.

@[simp]

theorem reesAlgebra.gradingZeroEquiv_apply {R : Type u} [CommRing R] (I : Ideal R) (p : ↥(grading I 0)) : (gradingZeroEquiv I) p = (↑↑p).coeff 0

@[simp]

theorem reesAlgebra.coe_gradingZeroEquiv_symm {R : Type u} [CommRing R] (I : Ideal R) (r : R) : ↑↑((gradingZeroEquiv I).symm r) = Polynomial.C r

@[simp]

theorem reesAlgebra.algebraMap_gradingZeroEquiv_symm {R : Type u} [CommRing R] (I : Ideal R) (r : R) : (algebraMap ↥(grading I 0) ↥(reesAlgebra I)) ((gradingZeroEquiv I).symm r) = (algebraMap R ↥(reesAlgebra I)) r

The constant-map triangle: R → grading I 0 → reesAlgebra I is algebraMap R (reesAlgebra I), where the second map is the grading-induced algebraMap (𝒜 0) A of Mathlib's SetLike.GradeZero instance (the one Proj.toSpecZero and fromZeroRingHom use).

instance reesAlgebra.isScalarTower_gradingZero {R : Type u} [CommRing R] (I : Ideal R) : IsScalarTower R ↥(grading I 0) ↥(reesAlgebra I)

The constant-map triangle as a scalar tower: the R-algebra structure of reesAlgebra I factors through its degree-zero piece.

theorem reesAlgebra.finiteType_of_fg {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) : Algebra.FiniteType ↥(grading I 0) ↥(reesAlgebra I)

For I finitely generated by g₁, …, gₖ, the Rees algebra is R[g₁t, …, gₖt] [Hau14, Definition 4.6], hence of finite type over its degree-zero piece for the grading-induced algebra structure — the hypothesis of Mathlib's IsProper (Proj.toSpecZero 𝒜). The finitely many degree-one generators of reesAlgebra.fg generate over grading I 0 because the two constant maps agree (reesAlgebra.algebraMap_gradingZeroEquiv_symm, the scalar tower).