[GOAL]
n : ℕ
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
[PROOFSTEP]
rw [← RingHom.ker_isRadical_iff_reduced_of_surjective (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),
  ZMod.ker_int_castRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero, Int.squarefree_coe_nat,
  Nat.cast_eq_zero]


[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ ⦃I : Ideal R⦄, Ideal.FG I → Injective ↑(lift (comp (lsmul R R) (Submodule.subtype I)))
[PROOFSTEP]
intro I _
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
⊢ Injective ↑(lift (comp (lsmul R R) (Submodule.subtype I)))
[PROOFSTEP]
rw [← Equiv.injective_comp (TensorProduct.rid R I).symm.toEquiv]
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
⊢ Injective
    (↑(lift (comp (lsmul R R) (Submodule.subtype I))) ∘
      ↑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.rid R { x // x ∈ I }))))
[PROOFSTEP]
convert Subtype.coe_injective using 1
[GOAL]
case h.e'_3
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
⊢ ↑(lift (comp (lsmul R R) (Submodule.subtype I))) ∘
      ↑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.rid R { x // x ∈ I }))) =
    fun a => ↑a
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
x : { x // x ∈ I }
⊢ (↑(lift (comp (lsmul R R) (Submodule.subtype I))) ∘
        ↑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.rid R { x // x ∈ I }))))
      x =
    ↑x
[PROOFSTEP]
simp only [Function.comp_apply, LinearEquiv.coe_toEquiv, rid_symm_apply, comp_apply, mul_one, lift.tmul,
  Submodule.subtype_apply, Algebra.id.smul_eq_mul, lsmul_apply]


[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ adjoin R ↑{X} = ⊤
[PROOFSTEP]
rw [Finset.coe_singleton]
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ adjoin R {X} = ⊤
[PROOFSTEP]
exact Polynomial.adjoin_X
[GOAL]
R : Type u_5
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
⊢ FiniteType R (MvPolynomial ι R)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_5
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι R)
[PROOFSTEP]
exact
  ⟨⟨Finset.univ.image MvPolynomial.X,
      by
      rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
      exact MvPolynomial.adjoin_range_X⟩⟩
[GOAL]
R : Type u_5
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R ↑(Finset.image MvPolynomial.X Finset.univ) = ⊤
[PROOFSTEP]
rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
[GOAL]
R : Type u_5
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range MvPolynomial.X) = ⊤
[PROOFSTEP]
exact MvPolynomial.adjoin_range_X
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
⊢ FiniteType A B
[PROOFSTEP]
obtain ⟨S, hS⟩ := hB.out
[GOAL]
case intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
⊢ FiniteType A B
[PROOFSTEP]
refine' ⟨⟨S, eq_top_iff.2 fun b => _⟩⟩
[GOAL]
case intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ b ∈ adjoin A ↑S
[PROOFSTEP]
have le : adjoin R (S : Set B) ≤ Subalgebra.restrictScalars R (adjoin A S) :=
  by
  apply (Algebra.adjoin_le _ : adjoin R (S : Set B) ≤ Subalgebra.restrictScalars R (adjoin A ↑S))
  simp only [Subalgebra.coe_restrictScalars]
  exact Algebra.subset_adjoin
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ adjoin R ↑S ≤ Subalgebra.restrictScalars R (adjoin A ↑S)
[PROOFSTEP]
apply (Algebra.adjoin_le _ : adjoin R (S : Set B) ≤ Subalgebra.restrictScalars R (adjoin A ↑S))
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ ↑S ⊆ ↑(Subalgebra.restrictScalars R (adjoin A ↑S))
[PROOFSTEP]
simp only [Subalgebra.coe_restrictScalars]
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
⊢ ↑S ⊆ ↑(adjoin A ↑S)
[PROOFSTEP]
exact Algebra.subset_adjoin
[GOAL]
case intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hB : FiniteType R B
S : Finset B
hS : adjoin R ↑S = ⊤
b : B
le : adjoin R ↑S ≤ Subalgebra.restrictScalars R (adjoin A ↑S)
⊢ b ∈ adjoin A ↑S
[PROOFSTEP]
exact le (eq_top_iff.1 hS b)
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ↑f
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
convert hRA.1.map f
[GOAL]
case h.e'_6
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ↑f
⊢ ⊤ = Subalgebra.map f ⊤
[PROOFSTEP]
simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using hf
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A ↔ ∃ s f, Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A → ∃ s f, Surjective ↑f
[PROOFSTEP]
rintro ⟨s, hs⟩
[GOAL]
case mp.mk.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ↑f
[PROOFSTEP]
use s, MvPolynomial.aeval (↑)
[GOAL]
case h
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Surjective ↑(MvPolynomial.aeval Subtype.val)
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
⊢ ∃ a, ↑(MvPolynomial.aeval Subtype.val) a = x
[PROOFSTEP]
have hrw : (↑s : Set A) = fun x : A => x ∈ s.val := rfl
[GOAL]
case h
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, ↑(MvPolynomial.aeval Subtype.val) a = x
[PROOFSTEP]
rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, ← hrw, hs]
[GOAL]
case h
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤
[PROOFSTEP]
exact Set.mem_univ x
[GOAL]
case mpr
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ s f, Surjective ↑f) → FiniteType R A
[PROOFSTEP]
rintro ⟨s, ⟨f, hsur⟩⟩
[GOAL]
case mpr.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
f : MvPolynomial { x // x ∈ s } R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
[PROOFSTEP]
exact FiniteType.of_surjective (FiniteType.mvPolynomial R { x // x ∈ s }) f hsur
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A ↔ ∃ ι x f, Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A → ∃ ι x f, Surjective ↑f
[PROOFSTEP]
rw [iff_quotient_mvPolynomial]
[GOAL]
case mp
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ s f, Surjective ↑f) → ∃ ι x f, Surjective ↑f
[PROOFSTEP]
rintro ⟨s, ⟨f, hsur⟩⟩
[GOAL]
case mp.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
f : MvPolynomial { x // x ∈ s } R →ₐ[R] A
hsur : Surjective ↑f
⊢ ∃ ι x f, Surjective ↑f
[PROOFSTEP]
use{ x : A // x ∈ s }, inferInstance, f
[GOAL]
case mpr
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ ι x f, Surjective ↑f) → FiniteType R A
[PROOFSTEP]
rintro ⟨ι, ⟨hfintype, ⟨f, hsur⟩⟩⟩
[GOAL]
case mpr.intro.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
[PROOFSTEP]
letI : Fintype ι := hfintype
[GOAL]
case mpr.intro.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
this : Fintype ι := hfintype
⊢ FiniteType R A
[PROOFSTEP]
exact FiniteType.of_surjective (FiniteType.mvPolynomial R ι) f hsur
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A ↔ ∃ n f, Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A → ∃ n f, Surjective ↑f
[PROOFSTEP]
rw [iff_quotient_mvPolynomial']
[GOAL]
case mp
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ ι x f, Surjective ↑f) → ∃ n f, Surjective ↑f
[PROOFSTEP]
rintro ⟨ι, hfintype, ⟨f, hsur⟩⟩
[GOAL]
case mp.intro.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
⊢ ∃ n f, Surjective ↑f
[PROOFSTEP]
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
[GOAL]
case mp.intro.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ n f, Surjective ↑f
[PROOFSTEP]
exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩
[GOAL]
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Surjective ↑(AlgHom.comp f ↑(AlgEquiv.symm equiv))
[PROOFSTEP]
simpa using hsur
[GOAL]
case mpr
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ n f, Surjective ↑f) → FiniteType R A
[PROOFSTEP]
rintro ⟨n, ⟨f, hsur⟩⟩
[GOAL]
case mpr.intro.intro
R : Type u_4
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
[PROOFSTEP]
exact FiniteType.of_surjective (FiniteType.mvPolynomial R (Fin n)) f hsur
[GOAL]
R : Type ?u.62480
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ Subalgebra.FG ⊤
[PROOFSTEP]
rw [← Subalgebra.prod_top]
[GOAL]
R : Type ?u.62480
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hA : FiniteType R A
hB : FiniteType R B
⊢ Subalgebra.FG (Subalgebra.prod ⊤ ⊤)
[PROOFSTEP]
exact hA.1.prod hB.1
[GOAL]
R✝ : Type ?u.66652
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R✝ A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R✝ B
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝ M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R✝ N
R : Type u_4
S : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing S
[PROOFSTEP]
obtain ⟨s, hs⟩ := h.1
[GOAL]
case intro
R✝ : Type ?u.66652
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R✝ A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R✝ B
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝ M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R✝ N
R : Type u_4
S : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ IsNoetherianRing S
[PROOFSTEP]
apply isNoetherianRing_of_surjective (MvPolynomial s R) S (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom
[GOAL]
case intro.hf
R✝ : Type ?u.66652
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R✝ A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R✝ B
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝ M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R✝ N
R : Type u_4
S : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ↑↑(MvPolynomial.aeval Subtype.val)
[PROOFSTEP]
erw [← Set.range_iff_surjective, ← AlgHom.coe_range, ← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype,
  Finset.setOf_mem, hs]
[GOAL]
case intro.hf
R✝ : Type ?u.66652
A : Type u
B : Type u_1
M : Type u_2
N : Type u_3
inst✝¹² : CommRing R✝
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R✝ A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R✝ B
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝ M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R✝ N
R : Type u_4
S : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
⊢ FiniteType (comp g f)
[PROOFSTEP]
let _ : Algebra A B := f.toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType (comp g f)
[PROOFSTEP]
let _ : Algebra A C := (g.comp f).toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra A C := toAlgebra (comp g f)
⊢ FiniteType (comp g f)
[PROOFSTEP]
exact
  Algebra.FiniteType.of_surjective hf
    { g with
      toFun := g
      commutes' := fun a => rfl }
    hg
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
hf : Surjective ↑f
⊢ FiniteType f
[PROOFSTEP]
rw [← f.comp_id]
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
hf : Surjective ↑f
⊢ FiniteType (comp f (RingHom.id A))
[PROOFSTEP]
exact (id A).comp_surjective hf
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
⊢ FiniteType (RingHom.comp g f)
[PROOFSTEP]
let _ : Algebra A B := f.toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType (RingHom.comp g f)
[PROOFSTEP]
let _ : Algebra A C := (g.comp f).toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ FiniteType (RingHom.comp g f)
[PROOFSTEP]
let _ : Algebra B C := g.toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : Algebra B C := toAlgebra g
⊢ FiniteType (RingHom.comp g f)
[PROOFSTEP]
exact
  @Algebra.FiniteType.trans A B C _ _ f.toAlgebra _ (g.comp f).toAlgebra g.toAlgebra
    ⟨by
      intro a b c
      simp [Algebra.smul_def, RingHom.map_mul, mul_assoc]
      rfl⟩
    hf hg
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : Algebra B C := toAlgebra g
⊢ ∀ (x : A) (y : B) (z : C), (x • y) • z = x • y • z
[PROOFSTEP]
intro a b c
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : Algebra B C := toAlgebra g
a : A
b : B
c : C
⊢ (a • b) • c = a • b • c
[PROOFSTEP]
simp [Algebra.smul_def, RingHom.map_mul, mul_assoc]
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : FiniteType g
hf : FiniteType f
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : Algebra B C := toAlgebra g
a : A
b : B
c : C
⊢ ↑(algebraMap B C) (↑(algebraMap A B) a) * (↑(algebraMap B C) b * c) = ↑(algebraMap A C) a * (↑(algebraMap B C) b * c)
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : FiniteType (RingHom.comp g f)
⊢ FiniteType g
[PROOFSTEP]
let _ := f.toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : FiniteType (RingHom.comp g f)
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType g
[PROOFSTEP]
let _ := g.toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : FiniteType (RingHom.comp g f)
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra B C := toAlgebra g
⊢ FiniteType g
[PROOFSTEP]
let _ := (g.comp f).toAlgebra
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : FiniteType (RingHom.comp g f)
x✝² : Algebra A B := toAlgebra f
x✝¹ : Algebra B C := toAlgebra g
x✝ : Algebra A C := toAlgebra (RingHom.comp g f)
⊢ FiniteType g
[PROOFSTEP]
let _ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : FiniteType (RingHom.comp g f)
x✝³ : Algebra A B := toAlgebra f
x✝² : Algebra B C := toAlgebra g
x✝¹ : Algebra A C := toAlgebra (RingHom.comp g f)
x✝ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
⊢ FiniteType g
[PROOFSTEP]
let _ : Algebra.FiniteType A C := h
[GOAL]
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : FiniteType (RingHom.comp g f)
x✝⁴ : Algebra A B := toAlgebra f
x✝³ : Algebra B C := toAlgebra g
x✝² : Algebra A C := toAlgebra (RingHom.comp g f)
x✝¹ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C
x✝ : Algebra.FiniteType A C := h
⊢ FiniteType g
[PROOFSTEP]
exact Algebra.FiniteType.of_restrictScalars_finiteType A B C
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ f ∈ adjoin R (of' R M '' ↑f.support)
[PROOFSTEP]
suffices span R (of' R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of' R M '' f.support)) by
  exact this (mem_span_support f)
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
this : span R (of' R M '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
⊢ f ∈ adjoin R (of' R M '' ↑f.support)
[PROOFSTEP]
exact this (mem_span_support f)
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ span R (of' R M '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : AddMonoidAlgebra R M
⊢ of' R M '' ↑f.support ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support)))
[PROOFSTEP]
exact subset_adjoin
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support) = ⊤
[PROOFSTEP]
refine' le_antisymm le_top _
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ⊤ ≤ adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support)
[PROOFSTEP]
rw [← hS, adjoin_le_iff]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support))
[PROOFSTEP]
intro f hf
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support))
[PROOFSTEP]
have hincl : of' R M '' f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' g.support :=
  by
  intro s hs
  exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
⊢ of' R M '' ↑f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
[PROOFSTEP]
intro s hs
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
s : AddMonoidAlgebra R M
hs : s ∈ of' R M '' ↑f.support
⊢ s ∈ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
[PROOFSTEP]
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
f : AddMonoidAlgebra R M
hf : f ∈ S
hincl : of' R M '' ↑f.support ⊆ ⋃ (g : AddMonoidAlgebra R M) (_ : g ∈ S), of' R M '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support))
[PROOFSTEP]
exact adjoin_mono hincl (mem_adjoin_support f)
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
[PROOFSTEP]
suffices (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of' R M '' (f.support : Set M)
  by
  rw [this]
  exact support_gen_of_gen hS
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
⊢ adjoin R (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
⊢ adjoin R (⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support) = ⊤
[PROOFSTEP]
exact support_gen_of_gen hS
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set (AddMonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support =
    ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), of' R M '' ↑f.support
[PROOFSTEP]
simp only [Set.image_iUnion]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
h : FiniteType R (AddMonoidAlgebra R M)
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤
[PROOFSTEP]
obtain ⟨S, hS⟩ := h
[GOAL]
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
S : Finset (AddMonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤
[PROOFSTEP]
letI : DecidableEq M := Classical.decEq M
[GOAL]
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
S : Finset (AddMonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤
[PROOFSTEP]
use Finset.biUnion S fun f => f.support
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
S : Finset (AddMonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ adjoin R (of' R M '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
[PROOFSTEP]
have : (Finset.biUnion S fun f => f.support : Set M) = ⋃ f ∈ S, (f.support : Set M) := by
  simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
S : Finset (AddMonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support
[PROOFSTEP]
simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
S : Finset (AddMonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (of' R M '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
[PROOFSTEP]
rw [this]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddCommMonoid M
S : Finset (AddMonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (of' R M '' ⋃ (f : AddMonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
[PROOFSTEP]
exact support_gen_of_gen' hS
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
⊢ of' R M m ∈ span R (of' R M '' S) ↔ m ∈ S
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Submodule.subset_span <| Set.mem_image_of_mem (of R M) h⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R (of' R M '' S)
⊢ m ∈ S
[PROOFSTEP]
erw [of', ← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
  Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
⊢ m ∈ closure S
[PROOFSTEP]
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' S) by simpa [← toSubmonoid_closure]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
this : ↑Multiplicative.ofAdd m ∈ Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
⊢ m ∈ closure S
[PROOFSTEP]
simpa [← toSubmonoid_closure]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
⊢ ↑Multiplicative.ofAdd m ∈ Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
[PROOFSTEP]
let S' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass S
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
S' : Submonoid (Multiplicative M) := Submonoid.closure S
⊢ ↑Multiplicative.ofAdd m ∈ Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
[PROOFSTEP]
have h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x : M => (of R M) x) '' S) := MonoidHom.map_mclosure _ _
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
S' : Submonoid (Multiplicative M) := Submonoid.closure S
h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => ↑(of R M) x) '' S)
⊢ ↑Multiplicative.ofAdd m ∈ Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
[PROOFSTEP]
rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
S' : Submonoid (Multiplicative M) := Submonoid.closure S
h : of' R M m ∈ span R ↑(Submonoid.map (of R M) S')
h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => ↑(of R M) x) '' S)
⊢ ↑Multiplicative.ofAdd m ∈ Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)
[PROOFSTEP]
simpa using of'_mem_span.1 h
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ↑(MvPolynomial.aeval fun s => of' R M ↑s)
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : AddMonoidAlgebra R M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = f
[PROOFSTEP]
induction' f using induction_on with m f g ihf ihg r f ih
[GOAL]
case hM
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd m)
[PROOFSTEP]
have : m ∈ closure S := hS.symm ▸ mem_top _
[GOAL]
case hM
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd m)
[PROOFSTEP]
refine' closure_induction this (fun m hm => _) _ _
[GOAL]
case hM.refine'_1
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd m)
[PROOFSTEP]
exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
[GOAL]
case hM.refine'_2
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd 0)
[PROOFSTEP]
exact ⟨1, AlgHom.map_one _⟩
[GOAL]
case hM.refine'_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    (∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd x)) →
      (∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd y)) →
        ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd (x + y))
[PROOFSTEP]
rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
[GOAL]
case hM.refine'_3.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => of' R M ↑s) P₁ = ↑(of R M) (↑Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => of' R M ↑s) P₂ = ↑(of R M) (↑Multiplicative.ofAdd m₂)
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(of R M) (↑Multiplicative.ofAdd (m₁ + m₂))
[PROOFSTEP]
exact ⟨P₁ * P₂, by rw [AlgHom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]; rfl⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => of' R M ↑s) P₁ = ↑(of R M) (↑Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => of' R M ↑s) P₂ = ↑(of R M) (↑Multiplicative.ofAdd m₂)
⊢ ↑(MvPolynomial.aeval fun s => of' R M ↑s) (P₁ * P₂) = ↑(of R M) (↑Multiplicative.ofAdd (m₁ + m₂))
[PROOFSTEP]
rw [AlgHom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => of' R M ↑s) P₁ = ↑(of R M) (↑Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => of' R M ↑s) P₂ = ↑(of R M) (↑Multiplicative.ofAdd m₂)
⊢ single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd m₁) + ↑Multiplicative.toAdd (↑Multiplicative.ofAdd m₂)) 1 =
    single (↑Multiplicative.toAdd (↑Multiplicative.ofAdd (m₁ + m₂))) 1
[PROOFSTEP]
rfl
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : AddMonoidAlgebra R M
ihf : ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = f
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = g
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = f + g
[PROOFSTEP]
rcases ihf with ⟨P, rfl⟩
[GOAL]
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : AddMonoidAlgebra R M
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = ↑(MvPolynomial.aeval fun s => of' R M ↑s) P + g
[PROOFSTEP]
rcases ihg with ⟨Q, rfl⟩
[GOAL]
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    ↑(MvPolynomial.aeval fun s => of' R M ↑s) a =
      ↑(MvPolynomial.aeval fun s => of' R M ↑s) P + ↑(MvPolynomial.aeval fun s => of' R M ↑s) Q
[PROOFSTEP]
exact ⟨P + Q, AlgHom.map_add _ _ _⟩
[GOAL]
case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : AddMonoidAlgebra R M
ih : ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = f
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = r • f
[PROOFSTEP]
rcases ih with ⟨P, rfl⟩
[GOAL]
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => of' R M ↑s) a = r • ↑(MvPolynomial.aeval fun s => of' R M ↑s) P
[PROOFSTEP]
exact ⟨r • P, AlgHom.map_smul _ _ _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommRing R
h : AddMonoid.FG M
⊢ FiniteType R (AddMonoidAlgebra R M)
[PROOFSTEP]
obtain ⟨S, hS⟩ := h.out
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommRing R
h : AddMonoid.FG M
S : Finset M
hS : closure ↑S = ⊤
⊢ FiniteType R (AddMonoidAlgebra R M)
[PROOFSTEP]
exact
  (FiniteType.mvPolynomial R (S : Set M)).of_surjective (MvPolynomial.aeval fun s : (S : Set M) => of' R M ↑s)
    (mvPolynomial_aeval_of_surjective_of_closure hS)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M
[PROOFSTEP]
refine' ⟨fun h => _, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
⊢ AddMonoid.FG M
[PROOFSTEP]
obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M
[PROOFSTEP]
refine' AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => _⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S
[PROOFSTEP]
have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
  simp only [hS, top_toSubmodule, Submodule.mem_top]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ of' R M m ∈ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
[PROOFSTEP]
simp only [hS, top_toSubmodule, Submodule.mem_top]
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S
[PROOFSTEP]
rw [adjoin_eq_span] at hm
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S
[PROOFSTEP]
exact mem_closure_of_mem_span_closure hm
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
G : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G
[PROOFSTEP]
simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ f ∈ adjoin R (↑(of R M) '' ↑f.support)
[PROOFSTEP]
suffices span R (of R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of R M '' f.support)) by
  exact this (mem_span_support f)
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
this : span R (↑(of R M) '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support))
⊢ f ∈ adjoin R (↑(of R M) '' ↑f.support)
[PROOFSTEP]
exact this (mem_span_support f)
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ span R (↑(of R M) '' ↑f.support) ≤ ↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support))
[PROOFSTEP]
rw [Submodule.span_le]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
f : MonoidAlgebra R M
⊢ ↑(of R M) '' ↑f.support ⊆ ↑(↑Subalgebra.toSubmodule (adjoin R (↑(of R M) '' ↑f.support)))
[PROOFSTEP]
exact subset_adjoin
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support) = ⊤
[PROOFSTEP]
refine' le_antisymm le_top _
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ⊤ ≤ adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support)
[PROOFSTEP]
rw [← hS, adjoin_le_iff]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
[PROOFSTEP]
intro f hf
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
[PROOFSTEP]
have hincl :
  (of R M '' f.support) ⊆
    Set.iUnion fun (g : MonoidAlgebra R M) => Set.iUnion fun (_ : g ∈ S) => (of R M '' g.support) :=
  by
  intro s hs
  exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
⊢ ↑(of R M) '' ↑f.support ⊆ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
[PROOFSTEP]
intro s hs
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
s : MonoidAlgebra R M
hs : s ∈ ↑(of R M) '' ↑f.support
⊢ s ∈ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
[PROOFSTEP]
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
f : MonoidAlgebra R M
hf : f ∈ S
hincl : ↑(of R M) '' ↑f.support ⊆ ⋃ (g : MonoidAlgebra R M) (_ : g ∈ S), ↑(of R M) '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support))
[PROOFSTEP]
exact adjoin_mono hincl (mem_adjoin_support f)
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ adjoin R (↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
[PROOFSTEP]
suffices (of R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of R M '' (f.support : Set M)
  by
  rw [this]
  exact support_gen_of_gen hS
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  ↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support =
    ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support
⊢ adjoin R (↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
this :
  ↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support =
    ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support
⊢ adjoin R (⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support) = ⊤
[PROOFSTEP]
exact support_gen_of_gen hS
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set (MonoidAlgebra R M)
hS : adjoin R S = ⊤
⊢ ↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support =
    ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑(of R M) '' ↑f.support
[PROOFSTEP]
simp only [Set.image_iUnion]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
h : FiniteType R (MonoidAlgebra R M)
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
[PROOFSTEP]
obtain ⟨S, hS⟩ := h
[GOAL]
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
[PROOFSTEP]
letI : DecidableEq M := Classical.decEq M
[GOAL]
case mk.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ∃ G, adjoin R (↑(of R M) '' ↑G) = ⊤
[PROOFSTEP]
use Finset.biUnion S fun f => f.support
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ adjoin R (↑(of R M) '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
[PROOFSTEP]
have : (Finset.biUnion S fun f => f.support : Set M) = ⋃ f ∈ S, (f.support : Set M) := by
  simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this : DecidableEq M := Classical.decEq M
⊢ ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
[PROOFSTEP]
simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (↑(of R M) '' ↑(Finset.biUnion S fun f => f.support)) = ⊤
[PROOFSTEP]
rw [this]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoid M
S : Finset (MonoidAlgebra R M)
hS : adjoin R ↑S = ⊤
this✝ : DecidableEq M := Classical.decEq M
this : ↑(Finset.biUnion S fun f => f.support) = ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support
⊢ adjoin R (↑(of R M) '' ⋃ (f : MonoidAlgebra R M) (_ : f ∈ S), ↑f.support) = ⊤
[PROOFSTEP]
exact support_gen_of_gen' hS
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
⊢ ↑(of R M) m ∈ span R (↑(of R M) '' S) ↔ m ∈ S
[PROOFSTEP]
refine' ⟨fun h => _, fun h => Submodule.subset_span <| Set.mem_image_of_mem (of R M) h⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑(of R M) m ∈ span R (↑(of R M) '' S)
⊢ m ∈ S
[PROOFSTEP]
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
  Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑(of R M) m ∈ span R ↑(closure (↑(of R M) '' S))
⊢ m ∈ closure S
[PROOFSTEP]
rw [← MonoidHom.map_mclosure] at h
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : CommMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑(of R M) m ∈ span R ↑(Submonoid.map (of R M) (closure S))
⊢ m ∈ closure S
[PROOFSTEP]
simpa using of_mem_span_of_iff.1 h
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s)
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : MonoidAlgebra R M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
[PROOFSTEP]
induction' f using induction_on with m f g ihf ihg r f ih
[GOAL]
case hM
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
[PROOFSTEP]
have : m ∈ closure S := hS.symm ▸ mem_top _
[GOAL]
case hM
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
[PROOFSTEP]
refine' closure_induction this (fun m hm => _) _ _
[GOAL]
case hM.refine'_1
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) m
[PROOFSTEP]
exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
[GOAL]
case hM.refine'_2
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) 1
[PROOFSTEP]
exact ⟨1, AlgHom.map_one _⟩
[GOAL]
case hM.refine'_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    (∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) x) →
      (∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) y) →
        ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) (x * y)
[PROOFSTEP]
rintro m₁ m₂ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
[GOAL]
case hM.refine'_3.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₁ = ↑(of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₂ = ↑(of R M) m₂
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(of R M) (m₁ * m₂)
[PROOFSTEP]
exact ⟨P₁ * P₂, by rw [AlgHom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
P₁ : MvPolynomial (↑S) R
hP₁ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₁ = ↑(of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P₂ = ↑(of R M) m₂
⊢ ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) (P₁ * P₂) = ↑(of R M) (m₁ * m₂)
[PROOFSTEP]
rw [AlgHom.map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : MonoidAlgebra R M
ihf : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = g
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f + g
[PROOFSTEP]
rcases ihf with ⟨P, rfl⟩
[GOAL]
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : MonoidAlgebra R M
ihg : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P + g
[PROOFSTEP]
rcases ihg with ⟨Q, rfl⟩
[GOAL]
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a =
      ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P + ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) Q
[PROOFSTEP]
exact ⟨P + Q, AlgHom.map_add _ _ _⟩
[GOAL]
case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : MonoidAlgebra R M
ih : ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = f
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = r • f
[PROOFSTEP]
rcases ih with ⟨P, rfl⟩
[GOAL]
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : MvPolynomial (↑S) R
⊢ ∃ a, ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) a = r • ↑(MvPolynomial.aeval fun s => ↑(of R M) ↑s) P
[PROOFSTEP]
exact ⟨r • P, AlgHom.map_smul _ _ _⟩
[GOAL]
R : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
G : Type u_3
inst✝² : CommGroup G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (MonoidAlgebra R G) ↔ Group.FG G
[PROOFSTEP]
simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
n : R[X]
a : M
⊢ HSMul R[X] M ((fun x => M) a)
[PROOFSTEP]
letI := modulePolynomialOfEndo f
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
n : R[X]
a : M
this : Module R[X] M := modulePolynomialOfEndo f
⊢ HSMul R[X] M ((fun x => M) a)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
⊢ SMul R[X] M
[PROOFSTEP]
letI := modulePolynomialOfEndo f
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
this : Module R[X] M := modulePolynomialOfEndo f
⊢ SMul R[X] M
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
⊢ IsScalarTower R R[X] M
[PROOFSTEP]
let _ := modulePolynomialOfEndo f
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ IsScalarTower R R[X] M
[PROOFSTEP]
constructor
[GOAL]
case smul_assoc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ ∀ (x : R) (y : R[X]) (z : M), (x • y) • z = x • y • z
[PROOFSTEP]
intro x y z
[GOAL]
case smul_assoc
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
x✝ : Module R[X] M := modulePolynomialOfEndo f
x : R
y : R[X]
z : M
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
⊢ Function.Injective ↑f
[PROOFSTEP]
let _ := modulePolynomialOfEndo f
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
⊢ Function.Injective ↑f
[PROOFSTEP]
haveI : IsScalarTower R R[X] M := modulePolynomialOfEndo.isScalarTower f
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
⊢ Function.Injective ↑f
[PROOFSTEP]
have hfgpoly : Finite R[X] M := Finite.of_restrictScalars_finite R _ _
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
⊢ Function.Injective ↑f
[PROOFSTEP]
have X_mul : ∀ o, (X : R[X]) • o = f o := by
  intro
  rw [modulePolynomialOfEndo_smul_def, aeval_X]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
⊢ ∀ (o : M), X • o = ↑f o
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
o✝ : M
⊢ X • o✝ = ↑f o✝
[PROOFSTEP]
rw [modulePolynomialOfEndo_smul_def, aeval_X]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
⊢ Function.Injective ↑f
[PROOFSTEP]
have : (⊤ : Submodule R[X] M) ≤ Ideal.span {(X : R[X])} • ⊤ :=
  by
  intro a ha
  obtain ⟨y, rfl⟩ := f_surj a
  rw [← X_mul y]
  exact Submodule.smul_mem_smul (Ideal.mem_span_singleton.mpr (dvd_refl _)) trivial
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
⊢ ⊤ ≤ Ideal.span {X} • ⊤
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
a : M
ha : a ∈ ⊤
⊢ a ∈ Ideal.span {X} • ⊤
[PROOFSTEP]
obtain ⟨y, rfl⟩ := f_surj a
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
y : M
ha : ↑f y ∈ ⊤
⊢ ↑f y ∈ Ideal.span {X} • ⊤
[PROOFSTEP]
rw [← X_mul y]
[GOAL]
case intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
y : M
ha : ↑f y ∈ ⊤
⊢ X • y ∈ Ideal.span {X} • ⊤
[PROOFSTEP]
exact Submodule.smul_mem_smul (Ideal.mem_span_singleton.mpr (dvd_refl _)) trivial
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
⊢ Function.Injective ↑f
[PROOFSTEP]
obtain ⟨F, hFa, hFb⟩ :=
  Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul _ (⊤ : Submodule R[X] M) (finite_def.mp hfgpoly) this
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFa : F - 1 ∈ Ideal.span {X}
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
⊢ Function.Injective ↑f
[PROOFSTEP]
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFa : F - 1 ∈ Ideal.span {X}
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
⊢ ∀ (m : M), ↑f m = 0 → m = 0
[PROOFSTEP]
intro m hm
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFa : F - 1 ∈ Ideal.span {X}
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
⊢ m = 0
[PROOFSTEP]
rw [Ideal.mem_span_singleton'] at hFa
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFa : ∃ a, a * X = F - 1
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
⊢ m = 0
[PROOFSTEP]
obtain ⟨G, hG⟩ := hFa
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
G : R[X]
hG : G * X = F - 1
⊢ m = 0
[PROOFSTEP]
suffices (F - 1) • m = 0 by
  have Fmzero := hFb m (by simp)
  rwa [← sub_add_cancel F 1, add_smul, one_smul, this, zero_add] at Fmzero
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝¹ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this✝ : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
G : R[X]
hG : G * X = F - 1
this : (F - 1) • m = 0
⊢ m = 0
[PROOFSTEP]
have Fmzero := hFb m (by simp)
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝¹ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this✝ : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
G : R[X]
hG : G * X = F - 1
this : (F - 1) • m = 0
⊢ m ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝¹ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this✝ : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
G : R[X]
hG : G * X = F - 1
this : (F - 1) • m = 0
Fmzero : F • m = 0
⊢ m = 0
[PROOFSTEP]
rwa [← sub_add_cancel F 1, add_smul, one_smul, this, zero_add] at Fmzero
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hfg : Finite R M
f_surj : Surjective ↑f
x✝ : Module R[X] M := modulePolynomialOfEndo f
this✝ : IsScalarTower R R[X] M
hfgpoly : Finite R[X] M
X_mul : ∀ (o : M), X • o = ↑f o
this : ⊤ ≤ Ideal.span {X} • ⊤
F : R[X]
hFb : ∀ (n : M), n ∈ ⊤ → F • n = 0
m : M
hm : ↑f m = 0
G : R[X]
hG : G * X = F - 1
⊢ (F - 1) • m = 0
[PROOFSTEP]
rw [← hG, mul_smul, X_mul m, hm, smul_zero]


[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]


[GOAL]
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hp : p ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q
[GOAL]
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
⊢ p / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
nth_rw 1 [hr]
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
rw [mul_comm, EuclideanDomain.mul_div_cancel _ pq0]
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
[PROOFSTEP]
exact r0
[GOAL]
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hq : q ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q
[GOAL]
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
nth_rw 1 [hr]
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
[PROOFSTEP]
rw [mul_comm, EuclideanDomain.mul_div_cancel _ pq0]
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p✝ q✝ p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
[PROOFSTEP]
exact r0
[GOAL]
R : Type ?u.6736
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (gcd a b * lcm a b) (a * b)
[PROOFSTEP]
rw [EuclideanDomain.gcd_mul_lcm]