English
Let R be a commutative ring, I an ideal of R, and f a polynomial in R[X]. Then f belongs to the Rees algebra of I if and only if each coefficient f_i lies in I^i.
Русский
Пусть R — коммутативное кольцо, I — идеал R, и f — многочлен над R. Тогда f принадлежит Rees-алгебре I тогда и только тогда, когда каждый коэффициент f_i принадлежит I^i.
LaTeX
$$$f \in \mathrm{reesAlgebra}(I) \iff \forall i, \ f_{i} \in I^{i}$$$
Lean4
/-- The Rees algebra of an ideal `I`, defined as the subalgebra of `R[X]` whose `i`-th coefficient
falls in `I ^ i`. -/
def reesAlgebra : Subalgebra R R[X] where
carrier := {f | ∀ i, f.coeff i ∈ I ^ i}
mul_mem' hf hg
i := by
rw [coeff_mul]
apply Ideal.sum_mem
rintro ⟨j, k⟩ e
rw [← Finset.mem_antidiagonal.mp e, pow_add]
exact Ideal.mul_mem_mul (hf j) (hg k)
one_mem'
i := by
rw [coeff_one]
split_ifs with h
· subst h
simp
· simp
add_mem' hf hg
i := by
rw [coeff_add]
exact Ideal.add_mem _ (hf i) (hg i)
zero_mem' _ := Ideal.zero_mem _
algebraMap_mem' r
i := by
rw [algebraMap_apply, coeff_C]
split_ifs with h
· subst h
simp
· simp
