English
Let R be a ring and N an R-module. Suppose there exists a set-valued map v from an index type ι into M and a linear map f: M → N such that span_R(range v) = ⊤, f ∘ v is linearly independent, and span_R(range (f ∘ v)) = ⊤. Then f is bijective.
Русский
Пусть R — кольцо, N — R-модуль. Предположим, что существует множество v: ι → M и линейное отображение f: M → N такое, что порождающее множество span_R(range v) = ⊤, линейно независима композиция f ∘ v и span_R(range (f ∘ v)) = ⊤. Тогда f биективно.
LaTeX
$$$\\operatorname{span}_R(\\operatorname{range} v) = \\top \\;\\land\\; \\operatorname{LinearIndependent}_R(f \\circ v) \\;\\land\\; \\operatorname{span}_R(\\operatorname{range}(f \\circ v)) = \\top \\Rightarrow \\text{Bijective}(f)$$$
Lean4
theorem bijective_of_linearIndependent_of_span_eq_top {N : Type*} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N}
{ι : Type*} {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) (hli : LinearIndependent R (f ∘ v))
(hsp : Submodule.span R (Set.range <| f ∘ v) = ⊤) : Function.Bijective f :=
by
refine ⟨LinearMap.injective_of_linearIndependent hv hli, ?_⟩
rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp
rwa [← range_eq_top]
