English
The isRepresentation-toEnd map is surjective onto End_R(M) when the span of b is all of M.
Русский
Отображение toEnd покрывает все End_R(M) при условии полного охвата b.
LaTeX
$$Matrix.isRepresentation.toEnd_surjective R b hb$$
Lean4
theorem toEnd_exists_mem_ideal (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) :
∃ M, Matrix.isRepresentation.toEnd R b hb M = f ∧ ∀ i j, M.1 i j ∈ I :=
by
have : ∀ x, f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b) :=
by
rw [Ideal.range_finsuppTotal, hb]
exact fun x => hI (LinearMap.mem_range_self f x)
choose bM' hbM' using this
let A : Matrix ι ι R := fun i j => bM' (b j) i
have : A.Represents b f := by
rw [Matrix.represents_iff']
dsimp [A]
intro j
specialize hbM' (b j)
rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'
exact
⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this, fun i j =>
(bM' (b j) i).prop⟩
