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
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
let _ := modulePolynomialOfEndo f
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
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
haveI : IsScalarTower R R[X] M := modulePolynomialOfEndo.isScalarTower f
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
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
have hfgpoly : Finite R[X] M := Finite.of_restrictScalars_finite R _ _
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
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
have X_mul : ∀ o, (X : R[X]) • o = f o := by
  intro
  rw [modulePolynomialOfEndo_smul_def, aeval_X]
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
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
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
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
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
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
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
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
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
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
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
intro m hm
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
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
rw [Ideal.mem_span_singleton'] at hFa
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
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
obtain ⟨G, hG⟩ := hFa
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
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
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
no goals
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
rw [← hG, mul_smul, X_mul m, hm, smul_zero]
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✝
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
intro
no goals
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✝
rw [modulePolynomialOfEndo_smul_def, aeval_X]
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} • ⊤
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} • ⊤
intro a ha
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} • ⊤
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} • ⊤
obtain ⟨y, rfl⟩ := f_surj a
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} • ⊤
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} • ⊤
rw [← X_mul y]
no goals
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} • ⊤
exact Submodule.smul_mem_smul (Ideal.mem_span_singleton.mpr (dvd_refl _)) trivial
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
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
have Fmzero := hFb m (by simp)
no goals
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
rwa [← sub_add_cancel F 1, add_smul, one_smul, this, zero_add] at Fmzero
no goals
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 ∈ ⊤
simp