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