[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
i : ℕ
⊢ coeff (a✝ * b✝) i ∈ I ^ i
[PROOFSTEP]
rw [coeff_mul]
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
i : ℕ
⊢ ∑ x in Finset.Nat.antidiagonal i, coeff a✝ x.fst * coeff b✝ x.snd ∈ I ^ i
[PROOFSTEP]
apply Ideal.sum_mem
[GOAL]
case a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
i : ℕ
⊢ ∀ (c : ℕ × ℕ), c ∈ Finset.Nat.antidiagonal i → coeff a✝ c.fst * coeff b✝ c.snd ∈ I ^ i
[PROOFSTEP]
rintro ⟨j, k⟩ e
[GOAL]
case a.mk
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
i j k : ℕ
e : (j, k) ∈ Finset.Nat.antidiagonal i
⊢ coeff a✝ (j, k).fst * coeff b✝ (j, k).snd ∈ I ^ i
[PROOFSTEP]
rw [← Finset.Nat.mem_antidiagonal.mp e, pow_add]
[GOAL]
case a.mk
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i}
i j k : ℕ
e : (j, k) ∈ Finset.Nat.antidiagonal i
⊢ coeff a✝ (j, k).fst * coeff b✝ (j, k).snd ∈ I ^ (j, k).fst * I ^ (j, k).snd
[PROOFSTEP]
exact Ideal.mul_mem_mul (hf j) (hg k)
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
⊢ coeff 1 i ∈ I ^ i
[PROOFSTEP]
rw [coeff_one]
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
⊢ (if 0 = i then 1 else 0) ∈ I ^ i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : 0 = i
⊢ 1 ∈ I ^ i
[PROOFSTEP]
subst h
[GOAL]
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ 1 ∈ I ^ 0
[PROOFSTEP]
simp
[GOAL]
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : ¬0 = i
⊢ 0 ∈ I ^ i
[PROOFSTEP]
simp
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf :
  a✝ ∈
    {
          toSubsemigroup :=
            { carrier := {f | ∀ (i : ℕ), coeff f i ∈ I ^ i},
              mul_mem' :=
                (_ :
                  ∀ {a b : R[X]},
                    a ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} →
                      b ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} → ∀ (i : ℕ), coeff (a * b) i ∈ I ^ i) },
          one_mem' := (_ : ∀ (i : ℕ), coeff 1 i ∈ I ^ i) }.toSubsemigroup.carrier
hg :
  b✝ ∈
    {
          toSubsemigroup :=
            { carrier := {f | ∀ (i : ℕ), coeff f i ∈ I ^ i},
              mul_mem' :=
                (_ :
                  ∀ {a b : R[X]},
                    a ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} →
                      b ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} → ∀ (i : ℕ), coeff (a * b) i ∈ I ^ i) },
          one_mem' := (_ : ∀ (i : ℕ), coeff 1 i ∈ I ^ i) }.toSubsemigroup.carrier
i : ℕ
⊢ coeff (a✝ + b✝) i ∈ I ^ i
[PROOFSTEP]
rw [coeff_add]
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf :
  a✝ ∈
    {
          toSubsemigroup :=
            { carrier := {f | ∀ (i : ℕ), coeff f i ∈ I ^ i},
              mul_mem' :=
                (_ :
                  ∀ {a b : R[X]},
                    a ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} →
                      b ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} → ∀ (i : ℕ), coeff (a * b) i ∈ I ^ i) },
          one_mem' := (_ : ∀ (i : ℕ), coeff 1 i ∈ I ^ i) }.toSubsemigroup.carrier
hg :
  b✝ ∈
    {
          toSubsemigroup :=
            { carrier := {f | ∀ (i : ℕ), coeff f i ∈ I ^ i},
              mul_mem' :=
                (_ :
                  ∀ {a b : R[X]},
                    a ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} →
                      b ∈ {f | ∀ (i : ℕ), coeff f i ∈ I ^ i} → ∀ (i : ℕ), coeff (a * b) i ∈ I ^ i) },
          one_mem' := (_ : ∀ (i : ℕ), coeff 1 i ∈ I ^ i) }.toSubsemigroup.carrier
i : ℕ
⊢ coeff a✝ i + coeff b✝ i ∈ I ^ i
[PROOFSTEP]
exact Ideal.add_mem _ (hf i) (hg i)
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
⊢ coeff (↑(algebraMap R R[X]) r) i ∈ I ^ i
[PROOFSTEP]
rw [algebraMap_apply, coeff_C]
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
⊢ (if i = 0 then ↑(algebraMap R R) r else 0) ∈ I ^ i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : i = 0
⊢ ↑(algebraMap R R) r ∈ I ^ i
[PROOFSTEP]
subst h
[GOAL]
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
⊢ ↑(algebraMap R R) r ∈ I ^ 0
[PROOFSTEP]
simp
[GOAL]
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i
[PROOFSTEP]
simp
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
⊢ f ∈ reesAlgebra I ↔ ∀ (i : ℕ), i ∈ support f → coeff f i ∈ I ^ i
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
⊢ ∀ (a : ℕ), coeff f a ∈ I ^ a ↔ a ∈ support f → coeff f a ∈ I ^ a
[PROOFSTEP]
intro a
[GOAL]
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
a : ℕ
⊢ coeff f a ∈ I ^ a ↔ a ∈ support f → coeff f a ∈ I ^ a
[PROOFSTEP]
rw [mem_support_iff, Iff.comm, imp_iff_right_iff, Ne.def, ← imp_iff_not_or]
[GOAL]
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
f : R[X]
a : ℕ
⊢ coeff f a = 0 → coeff f a ∈ I ^ a
[PROOFSTEP]
exact fun e => e.symm ▸ (I ^ a).zero_mem
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
i : ℕ
r : R
⊢ ↑(monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i
[PROOFSTEP]
simp (config := { contextual := true }) [mem_reesAlgebra_iff_support, coeff_monomial, ← imp_iff_not_or]
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n : ℕ
r : R
hr : r ∈ I ^ n
⊢ ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
induction' n with n hn generalizing r
[GOAL]
case zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n
r : R
hr : r ∈ I ^ Nat.zero
⊢ ↑(monomial Nat.zero) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ _
[GOAL]
case succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I ^ Nat.succ n
⊢ ↑(monomial (Nat.succ n)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
rw [pow_succ] at hr 
[GOAL]
case succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ↑(monomial (Nat.succ n)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
apply
  Submodule.smul_induction_on (p := fun r =>
    (monomial (Nat.succ n)) r ∈ Algebra.adjoin R (Submodule.map (monomial 1) I)) hr
[GOAL]
case succ.Hb
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ (r : R),
    r ∈ I →
      ∀ (n_1 : R), n_1 ∈ I ^ n → ↑(monomial (Nat.succ n)) (r • n_1) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
intro r hr s hs
[GOAL]
case succ.Hb
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝¹ : R
hr✝¹ : r✝¹ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ ↑(monomial (Nat.succ n)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
rw [Nat.succ_eq_one_add, smul_eq_mul, ← monomial_mul_monomial]
[GOAL]
case succ.Hb
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝¹ : R
hr✝¹ : r✝¹ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r✝ : R
hr✝ : r✝ ∈ I * I ^ n
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ ↑(monomial 1) r * ↑(monomial n) s ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
exact Subalgebra.mul_mem _ (Algebra.subset_adjoin (Set.mem_image_of_mem _ hr)) (hn hs)
[GOAL]
case succ.H1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ ∀ (x y : R),
    ↑(monomial (Nat.succ n)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
      ↑(monomial (Nat.succ n)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
        ↑(monomial (Nat.succ n)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
intro x y hx hy
[GOAL]
case succ.H1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : ↑(monomial (Nat.succ n)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : ↑(monomial (Nat.succ n)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ ↑(monomial (Nat.succ n)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
rw [monomial_add]
[GOAL]
case succ.H1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ I : Ideal R
n✝ : ℕ
r✝ : R
hr✝ : r✝ ∈ I ^ n✝
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → ↑(monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : ↑(monomial (Nat.succ n)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : ↑(monomial (Nat.succ n)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ ↑(monomial (Nat.succ n)) x + ↑(monomial (Nat.succ n)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
[PROOFSTEP]
exact Subalgebra.add_mem _ hx hy
[GOAL]
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
[PROOFSTEP]
apply le_antisymm
[GOAL]
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
[PROOFSTEP]
apply Algebra.adjoin_le _
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)
[PROOFSTEP]
rintro _ ⟨r, hr, rfl⟩
[GOAL]
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)
[PROOFSTEP]
exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])
[GOAL]
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
[PROOFSTEP]
rwa [pow_one]
[GOAL]
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)
[PROOFSTEP]
intro p hp
[GOAL]
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)
[PROOFSTEP]
rw [p.as_sum_support]
[GOAL]
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)
[PROOFSTEP]
apply Subalgebra.sum_mem _ _
[GOAL]
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)
[PROOFSTEP]
rintro i -
[GOAL]
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)
[PROOFSTEP]
exact monomial_mem_adjoin_monomial (hp i)
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : Ideal.FG I
⊢ Subalgebra.FG (reesAlgebra I)
[PROOFSTEP]
classical
obtain ⟨s, hs⟩ := hI
rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
use s.image (monomial 1)
rw [Finset.coe_image]
change _ = Algebra.adjoin R (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
rw [Submodule.map_span, Algebra.adjoin_span]
[GOAL]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : Ideal.FG I
⊢ Subalgebra.FG (reesAlgebra I)
[PROOFSTEP]
obtain ⟨s, hs⟩ := hI
[GOAL]
case intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Subalgebra.FG (reesAlgebra I)
[PROOFSTEP]
rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
[GOAL]
case intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Subalgebra.FG (Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s)))
[PROOFSTEP]
use s.image (monomial 1)
[GOAL]
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R ↑(Finset.image (↑(monomial 1)) s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))
[PROOFSTEP]
rw [Finset.coe_image]
[GOAL]
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (↑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Ideal.span ↑s))
[PROOFSTEP]
change _ = Algebra.adjoin R (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
[GOAL]
case h
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
⊢ Algebra.adjoin R (↑(monomial 1) '' ↑s) = Algebra.adjoin R ↑(Submodule.map (monomial 1) (Submodule.span R ↑s))
[PROOFSTEP]
rw [Submodule.map_span, Algebra.adjoin_span]
