English
If v is linearly independent and f: ι' ↪ ι, and range v is contained in the span of range (v ∘ f), then f is surjective.
Русский
Если v линейно независимо и f: ι'↪ ι, причём образа v охватывается через линейную оболочку образа v∘f, то f сюръективен.
LaTeX
$$$\\text{LinearIndependent }R\\ v \\rightarrow (f\\colon ι'\\hookrightarrow ι) \\rightarrow (\\operatorname{range} v \\subseteq \\operatorname{span}_R(\\operatorname{range}(v\\circ f))) \\rightarrow \\text{Surjective } f$$$
Lean4
theorem surjective_of_linearIndependent_of_span [Nontrivial R] (hv : LinearIndependent R v) (f : ι' ↪ ι)
(hss : range v ⊆ span R (range (v ∘ f))) : Surjective f :=
by
intro i
let repr : (span R (range (v ∘ f)) : Type _) → ι' →₀ R := (hv.comp f f.injective).repr
let l := (repr ⟨v i, hss (mem_range_self i)⟩).mapDomain f
have h_total_l : Finsupp.linearCombination R v l = v i :=
by
dsimp only [l]
rw [Finsupp.linearCombination_mapDomain]
rw [(hv.comp f f.injective).linearCombination_repr]
have h_total_eq : Finsupp.linearCombination R v l = Finsupp.linearCombination R v (Finsupp.single i 1) := by
rw [h_total_l, Finsupp.linearCombination_single, one_smul]
have l_eq : l = _ := hv h_total_eq
dsimp only [l] at l_eq
rw [← Finsupp.embDomain_eq_mapDomain] at l_eq
rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with ⟨i', hi'⟩
use i'
exact hi'.2
