ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ ∃ a, ↑(toEnd R b hb) a = f
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Function.Surjective ↑(toEnd R b hb)
intro f
case intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_3
inst✝³ : AddCommGroup M✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M✝
I : Ideal R
b : ι → M✝
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M✝
M : { x // x ∈ isRepresentation R b }
e : ↑(toEnd R b hb) M = f
⊢ ∃ a, ↑(toEnd R b hb) a = f
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ ∃ a, ↑(toEnd R b hb) a = f
obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)
no goals
case intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_3
inst✝³ : AddCommGroup M✝
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M✝
I : Ideal R
b : ι → M✝
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M✝
M : { x // x ∈ isRepresentation R b }
e : ↑(toEnd R b hb) M = f
⊢ ∃ a, ↑(toEnd R b hb) a = f
exact ⟨M, e⟩
no goals
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ LinearMap.range f ≤ ⊤ • ⊤
simp