case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I

case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) = reesAlgebra I
apply le_antisymm
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I
apply Algebra.adjoin_le _
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ ↑(monomial 1) r ∈ ↑(reesAlgebra I)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)
rintro _ ⟨r, hr, rfl⟩
no goals
case intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ ↑(monomial 1) r ∈ ↑(reesAlgebra I)
exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ r ∈ I ^ 1
rwa [pow_one]
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ p ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
intro p hp
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∑ i in support p, ↑(monomial i) (coeff p i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ p ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
rw [p.as_sum_support]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∀ (x : ℕ), x ∈ support p → ↑(monomial x) (coeff p x) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∑ i in support p, ↑(monomial i) (coeff p i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
apply Subalgebra.sum_mem _ _
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ ↑(monomial i) (coeff p i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∀ (x : ℕ), x ∈ support p → ↑(monomial x) (coeff p x) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
rintro i -
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ ↑(monomial i) (coeff p i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
exact monomial_mem_adjoin_monomial (hp i)