English
Let R be a commutative ring and I an ideal of R. The Rees algebra of I is the R-algebra generated by the degree-one monomials coming from I, i.e. the image of I under the map r ↦ rX in R[X]. Equivalently, the R-algebra adjoin of the set { iX : i ∈ I } equals Rees(I).
Русский
Пусть R — коммутативное кольцо и I — идеал кольца R. Реес-алгебра I есть порожденная по R подалгебра, сгенерированная мономами степени 1, полученными из элементов I: изображениями элементов iX при отображении i ↦ iX в R[X]. Иными словами, подалгебра над R, порождаемая множеством { iX | i ∈ I }, совпадает с Rees(I).
LaTeX
$$$\displaystyle \operatorname{adjoin}_R\bigl(\{ iX \;|\; i \in I\}\bigr) = \mathrm{reesAlgebra}(I).$$$
Lean4
theorem adjoin_monomial_eq_reesAlgebra :
Algebra.adjoin R (Submodule.map (monomial 1 : R →ₗ[R] R[X]) I : Set R[X]) = reesAlgebra I :=
by
apply le_antisymm
· apply Algebra.adjoin_le _
rintro _ ⟨r, hr, rfl⟩
exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])
· intro p hp
rw [p.as_sum_support]
apply Subalgebra.sum_mem _ _
rintro i -
exact monomial_mem_adjoin_monomial (hp i)
